The Coq mailing list

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

----- Mail original -----
> De: "Michiel Helvensteijn" 
> <mhelvens AT gmail.com>
> À: "Jacques-Henri Jourdan" 
> <jacques-henri.jourdan AT inria.fr>
> Cc: "Pierre Casteran" 
> <pierre.casteran AT labri.fr>,
>  "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Lundi 15 Juillet 2013 22:40:59
> Objet: Re: [Coq-Club] Fixpoint definition
> 
> On Mon, Jul 15, 2013 at 10:37 PM, Michiel Helvensteijn
> <mhelvens AT gmail.com>
>  wrote:
> 
> >> Well, but it does works when it is through pair then lst, but not
> >> through lst then pair, which is really confusing.
> >
> > As I understand it, your first example works because it
> > structurally
> > decreases on a `lst` parameter. A `lst` can "contain itself" by
> > definition.
> >
> > Your second example tries to decrease on a `pair`. As far as the
> > type
> > `pair` is concerned, the actual parameter is not structurally
> > smaller
> > than the formal parameter, it's just different.
> 
> With that in mind, what about the following solution?
> 
> Inductive lst :=
>   | Nil | Cons : nat_lst_pair -> lst
> with nat_lst_pair :=
>   | Both: nat -> lst -> nat_lst_pair.
> 
> Fixpoint test2 p :=
>   match p with
>     | Both _ Nil       => 0
>     | Both _ (Cons l)  => test2 l
>   end.
> 

This does work, but breaks the modularity of the pair type.

Thanks !

> --
> www.mhelvens.net
>