coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Vector head/tail proof

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: frederic.blanqui AT loria.fr
Cc: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Vector head/tail proof
Date: Mon, 26 May 2008 20:05:02 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

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

Very nice and easy--thanks.

Edsko

[Coq-Club] Vector head/tail proof, Edsko de Vries
- Re: [Coq-Club] Vector head/tail proof, frederic . blanqui
  - Re: [Coq-Club] Vector head/tail proof, Edsko de Vries
  - Re: [Coq-Club] Vector head/tail proof, Pierre Cast�ran
- Re: [Coq-Club] Vector head/tail proof, Matthieu Sozeau
  - Re: [Coq-Club] Vector head/tail proof, Edsko de Vries
    - Re: [Coq-Club] Vector head/tail proof, Matthieu Sozeau
- Re: [Coq-Club] Vector head/tail proof, Hugo Herbelin