# Defining Mutually Recursive functions in Coq

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?

-
Do you know about {struct x} in Fixpoint? It tells Coq which argument it is decreasing. But more importantly, the recursive call rgm r s2 is suspect. How can Coq tell that it won't loop forever? –  Andrej Bauer Feb 19 '13 at 9:29
@AndrejBauer Neither argument is always decreasing. We only know that some argument decreases every step. The (rgm r s2) step is okay because in "Star", we run (f (a::nil) tl) -- thus the length of the string is decreasing every time. –  theorems Feb 19 '13 at 9:49
You don't have to explain this to me, but to Coq :-) –  Andrej Bauer Feb 19 '13 at 9:55
@AndrejBauer: I was hoping to use you as a English to Coq compiler. –  theorems Feb 19 '13 at 17:19
The Coq Program facility is probably what you are looking for. –  Andrej Bauer Feb 19 '13 at 23:24

As stated in Coq Reference Manual (2.3)

in Fixpoint, the decreasing argument must be given (unless the function is not recursive), but it must not necessary be structurally decreasing.

Key word is structurally, Coq can't guess, which arguments is decreasing at each step of the recursion.

The reason for this is nicely described in Software Foundations

Since Coq is not just a functional programming language, but also a consistent logic, any potentially non-terminating function needs to be rejected. Here is an (invalid!) Coq program showing what would go wrong if Coq allowed non-terminating recursive functions:

 Fixpoint loop_false (n : nat) : False := loop_false n.


That is, propositions like False would become provable (e.g. loop_false 0 would be a proof of False), which would be a disaster for Coq's logical consistency.

-
Regarding your comment: "Coq can't guess, which arguments is decreasing at each step of the recursion." Not yet :) Me too I have access to some insider information and apparently it's a work-in-progress. –  NisaiVloot Mar 27 at 0:57
So it this behaviour will change in next versions? –  romantsegelskyi Mar 27 at 1:08
Can't tell that, ask the dev team (coq.inria.fr/community). –  NisaiVloot Mar 27 at 1:12