The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Hao-yang Wang 
<hywang AT pobox.com>:

Hello,

  In order to give the function TL access to x and xs as respective
principal arguments for T and TL, you can use the technique of
"nested fix-points". So the inner function body is in the scope
of both declarations.

 The example of tree definitions with lists is on page 404-405
of the Coq'Art. The recursor on such trees can be downloaded
from the book's site :

http://www/labri.fr/Perso/~casteran/CoqArt/induc-fond/SRC/chap14.v

Please look at the definition of ltree_ind2 (Section correct_ltree_ind)

Cheers,

Pierre




> Hi! Could somebody please point to me why I would get the error
> 'Recursive call to T has principal argument equal to "x" instead of xs'
> with the following definitions? Aren't both "x" and "xs" subterms of "l"?
>
> Thanks,
> Hao-yang Wang
>
>
> Require Import List.
>
> Inductive term (V F:Set): Set :=
>     | Var: V -> term V F
>     | App: F -> list (term V F) -> term V F.
>
> Definition term_ind2 (V F:Set) (P: term V F->Prop) (PL: list (term V
> F)->Prop)
>           (* term *) (tv: forall v, P (Var V F v))
>                      (ta: forall f ts, PL ts -> P (App V F f ts))
>      (* term list *) (lz: PL nil)
>                      (ls: forall x, (P x) -> forall xs, PL xs -> PL (x::xs))
> :=
> fix T (t: term V F): P t :=
>     match t return P t with
>     | Var v => tv v
>     | App f ts => ta f ts (TL ts)
>     end
> with TL (l: list (term V F)): PL l :=
>     match l return PL l with
>     | nil => lz
>     | x::xs => ls x (T x) xs (TL xs)
>     end
> for T.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.