The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

You need to generalize your statement, so that it makes sense for
vectors of any length.

For instance:

Parameter P : (Vector bool 2) -> Prop.

Definition PP (n : nat) : Vector bool n -> Prop :=
match n as n return  Vector bool  n -> Prop with
| (S (S O)) => fun p => (P p)
| _              => fun _ => True
end.

Goal forall n p, PP n p.
intros n p; case p; simpl; trivial;
 clear n p; intros n v [|]; case v; trivial;
 clear n v; intros n v [|]; case v; trivial.
...


Cheers,

B


Le 10 juil. 07 à 20:26, Param Jyothi Reddy a écrit :

> 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?
>
>
> I can use or elimination if i could build proof for:
>
> (forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v ==
> 11. However i am not sure how the proof term for this looks either.
>
> Can someone help me understand this?
>
> Thanks,
> Param
>
> --------------------------------------------------------
> 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