The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Hello,

 Some \thing about this example can alseo be found in the tutorial
on [co]-inductive definitions (from p 490

Pierre


http://www.labri.fr/perso/casteran/RecTutorial.pdf

Quoting 
frederic.blanqui AT loria.fr:

> On Mon, 26 May 2008, Edsko de Vries wrote:
>
> > This works quite nicely, but I got stuck in the following proof:
> >
> > Lemma vec_decompose : forall (n : nat) (v : vec (S n)),
> > v = vcons n (vhead n v) (vtail n v).
> >
> > Any hints?
>
> you may perhaps find some solution reusing CoLoR/Util/Vector/VecUtil.v
> available on http://color.loria.fr/.
>
> there, we have:
>
> Definition Vid n : vec n -> vec n :=
>   match n return vec n -> vec n with
>     | O => fun _ => Vnil
>     | _ => fun v => Vcons (Vhead v) (Vtail v)
>   end.
>
> Lemma Vid_eq : forall n (v : vec n), v = Vid v.
>
> Proof.
> destruct v; auto.
> Defined.
>
> Lemma VSn_eq : forall n (v : vec (S n)), v = Vcons (Vhead v) (Vtail v).
>
> Proof.
> intros. change (Vcons (Vhead v) (Vtail v)) with (Vid v). apply Vid_eq.
> Defined.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/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 Castéran