The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Indeed. However this solution has the drawback of having to use a fixpoint 
combinator, rather than the fix construct.

----- Mail original -----
> De: "Daniel Schepler" 
> <dschepler AT gmail.com>
> À: "Jacques-Henri Jourdan" 
> <jacques-henri.jourdan AT inria.fr>
> Cc: "Michiel Helvensteijn" 
> <mhelvens AT gmail.com>,
>  "Pierre Casteran" 
> <pierre.casteran AT labri.fr>,
>  "coq-club"
> <coq-club AT inria.fr>
> Envoyé: Mardi 16 Juillet 2013 02:42:43
> Objet: Re: [Coq-Club] Fixpoint definition
> 
> On Mon, Jul 15, 2013 at 1:16 PM, Jacques-Henri Jourdan
> <jacques-henri.jourdan AT inria.fr>
>  wrote:
> >>
> >> But it's structurally decreasing through both `lst` and `pair`,
> >> and
> >> basic `Fixpoint` only understands *really trivial* structural
> >> decreasing arguments.
> >>
> >
> > Well, but it does works when it is through pair then lst, but not
> > through lst then pair, which is really confusing.
> 
> Here's one way to define a recursion principle on pairs in A * mylist
> A:
> 
> Inductive mylist (A:Type) : Type :=
> | mynil : mylist A
> | mycons : A * mylist A -> mylist A.
> 
> Definition mylist_rect' {A:Type} (P:mylist A -> Type)
>   (Pnil : P (mynil A)) (Pcons : forall (x:A) (l:mylist A),
>                           P l -> P (mycons A (x, l))) :
>   forall l : mylist A, P l :=
> fix F (l : mylist A) : P l :=
> match l return P l with
> | mynil => Pnil
> | mycons (x, l') => Pcons x l' (F l')
> end.
> 
> Definition mylist_pair_rect {A:Type}
>   (P : A * mylist A -> Type) (Pnil : forall x:A, P (x, mynil A))
>   (Pcons : forall (x:A) (pr:A * mylist A), P pr -> P (x, mycons A
>   pr))
>   (pr : A * mylist A) : P pr.
> destruct pr as [x l].
> revert x.
> induction l using mylist_rect'.
> exact Pnil.
> intros.
> apply Pcons.
> apply IHl.
> Defined.
> 
> (* Which expands to: *)
> Definition mylist_pair_rect' {A:Type}
>   (P : A * mylist A -> Type) (Pnil : forall x:A, P (x, mynil A))
>   (Pcons : forall (x:A) (pr:A * mylist A), P pr -> P (x, mycons A
>   pr))
>   (pr : A * mylist A) : P pr :=
> let (x, l) as p return (P p) := pr in
>   mylist_rect' (fun m:mylist A => forall x:A, P (x, m))
>   Pnil
>   (fun (x':A) (l':mylist A) (IHl : forall x'':A, P (x'', l')) (x'':A)
>   =>
>   Pcons x'' (x', l') (IHl x'))
>   l x.
> --
> Daniel Schepler
>