The Coq mailing list

[Jesse Clayton <j89clayton89 AT gmail.com>]

The situation gets complicated if two decreasing arguments are brought
into play:

Require Import List.
Variable A : Type.
Variable e : A.
Variable exp : forall (i : nat), list A -> list A -> A.
Variable b c : list A.

Fixpoint repeat_list (i : nat) : list nat :=
match i with
  | 0 => nil
  | S i' => i :: (repeat_list i')
end.

Fixpoint f (i : nat)(T: list nat) : A :=
match T with
  | nil => e
  | a :: T' => (fix f2 (i : nat) :=
    match i with
      | 0 => e
      | S i' => exp i (map f2 (repeat_list i'))(map (fun i => f i T')
(repeat_list i'))
    end ) i
end.

Apparently, Coq does not see that in (map f2 (repeat_list i')), f2
gets a decreasing argument,
namely i'.
Does anyone see how to make this definition type-check?
Thanks for your feedback.

On 10/23/12, Paolo Tranquilli 
<tranquil AT cs.unibo.it>
 wrote:
> This is also an (accepted) equivalent formulation:
>
> 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
>   | _::T2 =>
>       exp T2 (exp T2 (f1 T2) (f2 T2)) (f2 T2)
> end.
>
>
> 2012/10/22 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.
>>
>