Mutual Recursion with function unfolding

Using Coq
1

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.
2

If you want to keep the version where one of your arguments is not syntactically structurally decreasing, I don’t think you will be able to use structural recursion to define your functions. However you should be able to define them by well-founded recursion: one trick that I saw a few times is to use the lexicographic ordering on the product A * nat where A is the type of the argument that structurally decreases at some point and nat is some kind of fuel to do internal mutual calls that do not decrease the main argument. In your example, you should “attach” the pair (x, 0) to f1 and (x,1) to f2 and the conditions for the functions to be well-defined will be
(x, 1) <^lex (S x, 0) for the recursive call in f1 and (S x, 0) <^lex (S x, 1) for the recursive call in f2 both of which you should be able to discharge. Alternatively you should be able to write a decreasing measure in this simple case (for instance 2*x for f1 and 2*x + 1 for f2).

Edit: Having a bit more time, I tried the solution I was proposing and realized it’s not currently supported by Equations:

From Equations Require Import Equations.

Fail Equations f1 (x : nat) : nat by wf (2 * n + 1) lt :=
{ f1 0     := 0;
  f1 (S x) := f2 x }
where f2 (x : nat) : nat by wf (2 * n) lt :=
{ f2 0     := 0;
  f2 (S x) := f1 (S x) }.
(* The command has indeed failed with message:
   Mutual well-founded definitions are not supported *)

but the following encoding works

From Equations Require Import Equations.
From Coq Require Import micromega.Lia.

Equations? f (b : bool) (x : nat) : nat by wf (if b then 2 * x else 2 * x + 1) lt :=
  f true 0 := 0 ;
  f true (S x) := f false x ;
  f false 0 := 0 ;
  f false (S x) := f true (S x).
Proof. all: lia. Qed.

Notation f1 := (f true).
Notation f2 := (f false).
3

Hi kyod. I also noticed that well-founded mutual recursion is not yet supported. The encoding with bool as additional parameter is nice. I actually have a parameter (and return type) that has different types in the two functions. Of course, that could be done with if b then type1 else type2.

It is also possible in Equations to derive the functional induction lemma. For example, the following is a proof of what I proved above:

Lemma f12_correct b :
  (forall x, f b x = 0).
Proof.
  intros x. apply_funelim (f b x). (* I am not sure whether this is the right way to apply funelim *)
  all: congruence.
Qed.

I have already implemented the approach from the original post. I have defined the functional induction lemmas, but Combined Scheme failed. I will report an issue.

Perhaps using Equations is the best idea currently.

4

I found a relatively elegant way to write this on StackOverflow:

Definition f2' (f1 : nat -> nat) (x : nat) : nat :=
    match x with
    | 0 => 0
    | (S x as y) => f1 y
    end.

Fixpoint f1 (x : nat) { struct x } : nat :=
    let f2 := f2' f1 in
    match x with
    | 0 => 0
    | S x => f2 x
    end.

Definition f2 := f2' f1.
5

But could anyone explain what technical difficulty prevents termination checking with function unfolding for mutual recursion like this?

Axiom A : Type.
Axiom f g : nat -> nat.

Fixpoint foo (l : list A) : nat :=
  match l with
  | _ :: l' => f (bar l')
  | nil => 0
  end
with bar (l : list A) : nat :=  
  g (foo l).