The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 21 Oct 2012 01:44:03 +0300,
Jesse Clayton 
<j89clayton89 AT gmail.com>
 a écrit :

> Hi,
> 
> I wish to define function f1:
> 
> Require Import List.
> Variable exp: forall (T: list nat), Type -> Type -> Type.
> Variable b c: Type.
> 
> Fixpoint f1 (T: list nat):  Type:=
> match T with
>   | nil => exp nil b c
>   | _::T2 =>
>       exp T2 (f1 T2) (f2 T2)
>   end
> 
> with f2 (T: list nat): Type:=
> match T with
>   | nil => exp nil b c
>   | n::T2 =>
>       exp T2 (f1 T) (f2 T2)
> end.
> 
> but Coq returns "Recursive of f2 is ll-formed.". Do you have any idea
> how to solve this?
> Thanks a lot.

For the explanation of the error,

> with f2 (T: list nat): Type:=
> match T with
>   | nil => exp nil b c
>   | n::T2 =>
>       exp T2 (f1 T) (f2 T2)
                ^^^^
> end.

In this call, the argument of the recursion (T) is not strictly smaller
than the one of the definition (T).
Maybe you mistyped it and wanted to write "(f1 T2)" instead.
Else, you have to explain to Coq why your recursion is well founded.
===========================================
Require Import List.
Variable exp: forall (T: list nat), Type -> Type -> Type.
Variable b c: Type.

Definition f2_aux (f1 : list nat -> Type) : list nat -> Type:=
fix f2 (T : list nat) : Type :=
match T with
  | nil => exp nil b c
  | n::T2 =>
      exp T2 (f1 T) (f2 T2)
end.


Fixpoint f1 (T: list nat):  Type:=
match T with
  | nil => exp nil b c
  | _::T2 =>
      exp T2 (f1 T2) (f2_aux f1 T2)
  end.

Definition f2 : list nat -> Type := f2_aux f1.
==========================================
In this version, all recursive calls are enough explicitely smaller for
the Coq system. This is accepted, although it is probably not as nice
as what you would have expected.