Stream: Coq users

Topic: Mutually recursive Fixpoint strange behavior

Jules Viennot (May 14 2024 at 12:54):

Hello, working with mutually recursive Fixpoint led me to find this interesting and strange behavior :

Inductive P (A : Type) : Type :=
    | PI : A -> P A.
Arguments PI {A}.

Inductive E (A : Type) : Type :=
    | EZ : A -> E A
    | ES : P (E A) -> E A.
Arguments EZ {A}.
Arguments ES {A}.

Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
    match e with
    | EZ _ => 0
    | ES p => 1 + occ_p p
    end

with occ_p {A} (p : P (E A)) {struct p} : nat :=
    match p with
    | PI e => 1 + occ_e e
    end.

This simple mutually recursive Fixpoint on E and P simply counts the number of occurrences of ES and PI constructors along an element of E. But when trying to verify this function with Coq, I get the error message :

Recursive definition of occ_p is ill-formed.
In environment
occ_e : forall A : Type, E A -> nat
occ_p : forall A : Type, P (E A) -> nat
A : Type
p : P (E A)
e : E A
Recursive call to occ_e has principal argument equal to "e" instead of a subterm of "p".
Recursive definition is: "fun (A : Type) (p : P (E A)) => match p with
| PI e => 1 + occ_e A e
end".

I don't quite get the error message because it is straight forward that e is a subterm of p. Is it a wrong behavior from Coq or is the error message just bad ?

Gaëtan Gilbert (May 14 2024 at 13:00):

This is a classic problem with nested inductives, it doesn't understand fixpoints on the wrapper inductive P which call a mutual fixpoint on E. Instead you have to use a nested fixpoint:

Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
    match e with
    | EZ _ => 0
    | ES p =>
        let fix occ_p {A} (p : P (E A)) {struct p} : nat :=
          match p with
          | PI e => 1 + occ_e e
          end
        in
        1 + occ_p p
    end.

Definition occ_p {A} (p : P (E A)) : nat :=
  match p with
  | PI e => 1 + occ_e e
  end.

Jules Viennot (May 14 2024 at 15:32):

And if I want to use Equations for the job, is there a way to overcome this issue ?

Thomas Lamiaux (May 14 2024 at 16:14):

It is a bit complicated because the solution of Gaëtan inline the definition, so you don't really define functions by mutual induction anymore. If you want to do as Gaëtan did, it should indeed make it easier as Equations enables to write it almost as above an inline it automatically:

From Equations Require Import Equations.

Equations occ_e {A} (e : E A) : nat :=
occ_e (EZ _) => 0;
occ_e (ES p) => 1 + occ_p p

where occ_p (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.

Equations occ_p  (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.

Require Import Extraction.
Extraction occ_e.

Thomas Lamiaux (May 14 2024 at 16:18):

But if you try to define them by mutual recursion as before, it fails

Fail Equations occ_e {A} (e : E A) : nat :=
occ_e (EZ _) => 0;
occ_e (ES p) => 1 + occ_p p

with occ_p {A} (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.

Thomas Lamiaux (May 14 2024 at 16:18):

And I don't think you can cheat and use well-founded recursion because to the best of my knowledge, it is not supported for mutual definitions

Thomas Lamiaux (May 14 2024 at 16:19):

There might be a less direct technique but I am not aware of it

Pierre Courtieu (May 14 2024 at 16:37):

AFAIK mutual fixpoints are only allowed with all struct arguments on the same inductive family. So if P and E were mutual. But in this particular case you will have a strict positivity check error.

Dominique Larchey-Wendling (May 15 2024 at 10:38):

This works as well

Inductive P (A : Type) : Type :=
    | PI : A -> P A.
Arguments PI {A}.

Inductive E (A : Type) : Type :=
    | EZ : A -> E A
    | ES : P (E A) -> E A.
Arguments EZ {A}.
Arguments ES {A}.

Definition occ_p_gen {A} (f : A -> nat) (p : P A) :=
  match p with
  | PI e => 1 + f e
  end.

Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
  match e with
  | EZ _ => 0
  | ES p => occ_p_gen occ_e p
  end.

Definition occ_p {A} := occ_p_gen (@occ_e A).

Last updated: Oct 13 2024 at 01:02 UTC