This question is related to (but not the same as):How to define a function inductively on two arguments in Coq?In particular, I used those techniques (defining a second fixed point function) and Coq still complains.Consider the following formalization of regular expressions.Inductive symbol : Set := Zero | One.Definition string := list symbol.Fixpoint symbol_eq (a:symbol) (b:symbol) : bool :=  match a with    Zero =>    match b with      Zero => true    | One => false    end  | One =>    match b with      Zero => false    | One => true    end  end.Inductive regexp : Set :=    Symbol (s:symbol)  | Concat (r1:regexp) (r2:regexp)  | Union (u1:regexp) (u2:regexp)  | Star (u1:regexp)  .Fixpoint rgm (r:regexp) (s:string) :=  match r with    Symbol ss =>      match s with        nil => false      | a::nil => (symbol_eq ss a)      | a::b::tl => false      end   | Union r1 r2 => (orb (rgm r1 s) (rgm r2 s))   | Concat r1 r2 =>       let fix f s1 s2 :=         match s2 with           nil => (andb (rgm r1 (rev s1)) (rgm r2 s2))         | a::tl => (orb (andb (rgm r1 (rev s1)) (rgm r2 s2))                         (f (a::s1) tl))         end       in (f nil s)   | Star r1 =>       match s with         nil => true       | a::tl =>         let fix f s1 s2 :=           match s2 with             nil => (rgm r1 (rev s1))           | a::tl => (orb (andb (rgm r1 (rev s1)) (rgm r s2))                           (f (a::s1) tl))           end         in (f (a::nil) tl)       end  end.Coq refuses to compile it for the following reason:Error: Cannot guess decreasing argument of fix.Question: how can we fix this?
Defining Mutually Recursive functions in Coq
pl.programming languages;coq