Hi all,

I have mutually recursively defined functions. In one case, the second function calls the first function, but *not* with a syntactically smaller element. In non-mutually recursive functions, Coq’s guardedness checker usually unfolds *other* definitions, but it seems to not unfold the definitions we are trying to define.

Here’s my MWE. Note that my actual function is a bit more complex, so the solutions in `Module Test1`

and `Module Test2`

maybe not scale good to ‘bigger’ functions.

```
From Coq Require Import FunInd.
From Equations Require Import Equations.
Module Test1.
(** My actual function looks like this. In one case we recursively call the first function. *)
(** We don't call it on a syntactically smaller element, but if we unfold [f1] here, it could be defined. *)
Unset Guard Checking.
Fixpoint f1 (x : nat) { struct x } : nat :=
match x with
| 0 => 0
| S x => f2 x
end
with f2 (x : nat) { struct x } : nat :=
match x with
| 0 => 0
| S x => f1 (S x) (* This unfolds to [f2 x], and should be guarded thus *)
end.
(** Also, I would like to build a functional scheme. The FunInd package doesn't work here: *)
Fail Functional Scheme f1_ind := Induction for f1 Sort Prop
with f2_ind := Induction for f2 Sort Prop.
(* The command has indeed failed with message: *)
(* Cannot define graph(s) for f1, f2 *)
Set Guard Checking.
(** We can prove the lemma by manually, of course. However, this would be very tedious for 'big' functions *)
Section f1_f2_ind.
Variables (P1 P2 : nat -> nat -> Prop)
(H1: P1 0 0)
(H2: forall x y, P2 x y -> P1 (S x) y)
(H3: P2 0 0)
(H4: forall x y, P1 (S x) y -> P2 (S x) y).
Fixpoint f1_ind (x : nat) { struct x} : P1 x (f1 x)
with f2_ind (x : nat) { struct x } : P2 x (f2 x).
Proof.
- destruct x.
+ apply H1.
+ cbn. apply H2. eapply f2_ind.
- destruct x.
+ apply H3.
+ apply H4. cbn. apply H2. apply f2_ind.
Qed.
(** Note that this definition is guarded, because in case [f2 (S x)] I use the IH for [f2 x] *)
End f1_f2_ind.
(** We can build a combined scheme! *)
Combined Scheme f1_f2_ind from f1_ind, f2_ind.
(** And now, let's try to prove something *)
Lemma f1_f2_correct : (forall x, f1 x = 0) /\ (forall x, f2 x = 0).
Proof. apply f1_f2_ind with (P1 := fun x y => y = 0) (P2 := fun x y => y = 0); congruence. Qed.
End Test1.
Module Test2.
(** Of course, we can define [f1] and [f2] manually, by unfolding the definition of [f1] in [f2]: *)
Fixpoint f2 (x : nat) { struct x } : nat :=
match x with
| 0 => 0
| S x =>
let f1 := fun xs =>
match x with
| 0 => 0
| S x => f2 x
end in
f1 (S x)
end.
Definition f1 (x : nat) : nat :=
match x with
| 0 => 0
| S x => f2 x
end.
Lemma f2_eq (x : nat) :
f2 x =
match x with
| 0 => 0
| S x => f1 (S x)
end.
Proof. induction x; cbn; f_equal; auto. Qed.
(** Now, we could proceed like above... *)
End Test2.
Module Test3.
(** The Equations package doesn't help, unfortunately. Also, mutual wf recursion isn't supported. *)
Fail Equations f1 (x : nat) : nat :=
{ f1 0 := 0;
f1 (S x) := f2 x }
where f2 (x : nat) : nat :=
{ f2 0 := 0;
f2 (S x) := f1 (S x) }.
(* The command has indeed failed with message: *)
(* Recursive definition of f1 is ill-formed. *)
(* In environment *)
(* f1 : nat -> nat *)
(* x : nat *)
(* n : nat *)
(* n0 : nat *)
(* Recursive call to f1 has principal argument equal to "S n0" instead of one of the following variables: "n" *)
(* "n0". *)
(* Recursive definition is: *)
(* "fun x : nat => match x with *)
(* | 0 => 0 *)
(* | S n => (fun x0 : nat => match x0 with *)
(* | 0 => 0 *)
(* | S n0 => f1 (S n0) *)
(* end) n *)
(* end". *)
End Test3.
(** Here is an even more minimalised version without mutally recursive functions *)
Module Test4.
Fail Fixpoint f (x : nat) : nat :=
match x with
| 0 => 0
| 1 => 0
| S (S x) => f (S x)
end.
(* The command has indeed failed with message: *)
(* Recursive definition of f is ill-formed. *)
(* In environment *)
(* f : nat -> nat *)
(* x : nat *)
(* n : nat *)
(* x0 : nat *)
(* Recursive call to f has principal argument equal to "S x0" instead of one of the following variables: "n" "x0". *)
(* Recursive definition is: "fun x : nat => match x with *)
(* | S (S x0) => f (S x0) *)
(* | _ => 0 *)
(* end". *)
(** Of course, we can use the approach from [Test2] again and unfold the definition *)
Fixpoint f (x : nat) : nat :=
match x with
| 0 => 0
| 1 => 0
| S (S _ as y) =>
let f := fun x =>
match x with
| 0 => 0
| 1 => 0
| S (S _ as y) => f y
end in
f y
end.
(** But from here, I would again have to define my FunInd scheme again... *)
(** For the record, note that [f] can be implemented more elegantly: *)
Fixpoint f' (x : nat) : nat :=
match x with
| 0 => 0
| 1 => 0
| S (S _ as y) => f' y
end.
End Test4.
```