The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 10 Jul 2007, Param Jyothi Reddy wrote:

> Hi,
> Lets define vector in usual way with constructors:
> nil : Vector T 0
> cons : Vector T n -> T -> Vector T (S n)
>
> along with its inductive elimination rule. Let BD be type of Binary
> Digits (enumeration with elements 0 and 1).
>
> Also lets say i have proofs of some predicate P for all elements of
> Vector's over BD of length 2, i.e.
>
> p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons
> (cons nil d) b.
>
> using these How will the proof term for
>
> (forall v : Vector BD (S S 0) ). P(v) look like?

Here is one way to prove it, but I use the lemmas VSn_eq and V0_eq, so it 
may not answer the question you are asking.

Require Import Bvector.

Section V.

Variable P : vector bool 2 -> Prop.
Hypothesis P0 : P (Vcons _ false _ (Vcons _ false _ (Vnil _))).
Hypothesis P1 : P (Vcons _ false _ (Vcons _ true _ (Vnil _))).
Hypothesis P2 : P (Vcons _ true _ (Vcons _ false _ (Vnil _))).
Hypothesis P3 : P (Vcons _ true _ (Vcons _ true _ (Vnil _))).

Lemma HP : forall (v:vector bool 2), P v.
Proof.
intros v.
rewrite VSn_eq.
generalize (Vhead bool 1 v) (Vtail bool 1 v).
clear v.
intros b0 v0.
rewrite (VSn_eq _ _ v0).
rewrite (V0_eq _ (Vtail bool 0 v0)).
generalize (Vhead bool 0 v0).
clear v0.
intros b1.
destruct b0; destruct b1; assumption.
Qed.


--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''