The Coq mailing list

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

Le Tue, 30 Oct 2012 00:36:50 +0100,
Jesse Clayton 
<j89clayton89 AT gmail.com>
 a écrit :

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

You can only decrease on one argument.

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

Your f function is needlessly complicate, I even bet it does not do
what you wish. For instance the 'a' is not even used.

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

You can still provide some upperbound.

Require Import List.

Module Type Test.
 Parameter A : Type.
 Parameter e : A.
 Parameter exp : forall (i : nat), list A -> list A -> A.
(* Parameter b c : list A.*)
End Test.

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

 Fixpoint f (k : nat) (i : nat) (T: list nat) {struct k} : T.A :=
 match T with
   | nil => T.e
   | a :: T' =>
     let f := match k with O => fun _ _ => T.e | S k => f k end in
    (fix f2 (k : nat) (i : nat) {struct k} : T.A :=
     match i with
       | 0 => T.e
       | S i' =>
         let f2 := match k with O => fun _ => T.e | S k => f2 k end
         in
         T.exp i (map f2 (repeat_list i'))
                       (map (fun i => f i T') (repeat_list i'))
       end) k i
 end.
End Test2.

Module Essai.
 Inductive Free := Leaf : Free | Node : nat -> list Free -> list Free
-> Free. Definition A : Type := Free.
 Definition e : A := Leaf.
 Definition exp : nat -> list A -> list A -> A := Node.
End Essai.

Module Essai2 := Test2 Essai.

Eval compute in (Essai2.f 10000 5 (3::4::2::nil)).

***************************
There, the upper_bound for f2 is 'i' itself, and for f, you have to
compute it.

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