[TYPES] [Coq-Club] Proof term for proof by exhaustion

[Param Jyothi Reddy]

Hi Benjamin,
I wanted to look at how the actual proof term (in terms of raw CIC/PTS
type system) looks like rather than using tactics. More from
perspective of understanding type system.

The essential point is how can we express the fact that vector of
length 2 are just 00,01,10 and 11 (nothing more/nothing less)?

Param

On 7/10/07, Benjamin Werner <benjamin.werner at inria.fr> wrote:
> 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
>
>