The Coq mailing list

[casteran AT labri.fr]

Selon june andronick 
<jandronick AT axalto.com>:


Hi June,

 I have written (in a bad style, but it's late and November 11th is
 a holiday :-) ) a solution to your problem. I will put in in a better
form and add it as an exercise.

 I use the trick given in this club by Yves Bertot, Pierre Letouzey
and Laurent Thery : prove somme decomposition lemmas about vectors
of length 0, 1, S n ..., expressed with head and tails.
I rather defined nth as a partial function, but you will find at the
end of the file a proof of equivalence with your definition. It is certainly
possible to use only your inductive definition of nth ...

About dependent elimination and its subtleties , I must recommand to read the
beautiful pages Yves has written for the book.

Attached is the development (DRAFT).
Notice that I put two "Admitted" in this development, to be replaced
by the proofs by Pierre and Laurent (in the Club archive).

Pierre




> Hello,
>
> I have some difficulties while using dependant types, more precisely when
> defining inductive predicate and doing inversion on them. An hypothesis of
> the form:
>       H : existS (fun x : T1 => T2) y v1 = existS (fun x : T1 => T2) y v2
> appears and sometimes v2 as been changed into v1 in my goal (after
> simplification of projs2(existS ...)), but sometimes no and I cannot deduce
> anything like v1=v2 (injection doesn't work...). And in my goal I have a
> "match...in...return...with...end" form that I don't really understand (I
> don't really understand the "in..." part)...
>
> Since I'm not very familiar with dependant types, I cannot say whether it
> comes from my definitions or if it's a theoretical problem ... I would be
> grateful if someone can give me some indications.
> Hereafter is the whole problem (sorry if it's a bit long, I didn't manage to
> explain it in a shorter manner)
>
> Thanks in advance
> June Andronick
> --------------------------------------------------------------
> (* I have the following definition of lists of size n : *)
>      Inductive listn : nat -> Set :=
>        | niln : listn 0
>        | consn : forall n:nat, nat -> listn n -> listn (S n).
>
> (* I defined a predicate for the ith element of the list : *)
>      Inductive ith :
>         forall (n:nat), listn (S n) -> nat ->  nat -> Prop :=
>         | IthBitFirst : forall (nn:nat) (elt:nat) (tl:listn nn),
>                         (ith nn (consn nn elt tl) 0 elt)
>         | IthBitNotFirst :
>             forall (nn:nat) (elt:nat) (tl:listn (S nn)) (i:nat) (res:nat),
>             (ith nn tl i res) ->
>             (ith (S nn) (consn (S nn) elt tl) (S i) res) .
>
> (* The case where it works : *)
>      Parameter un_op : nat -> nat.
>      Fixpoint listn_un_op (n:nat)(l:listn n){struct l}: listn n :=
>        match l in listn n return listn n with
>         | niln => niln
>         | consn n' a y => consn n' (un_op a) (listn_un_op n' y)
>         end.
>
>      Lemma ith_of_listn_un_op :
>      forall i n l res,
>      (ith n l i res) ->
>      (ith n (listn_un_op (S n) l) i (un_op res)).
>      Proof.
>        induction i; intros; inversion H; simpl; subst; constructor.
>        apply (IHi nn tl res); auto.
>      Qed.
>
> (* The case where it doesn't work *)
> (* (by the way, I didn't manage to define listn_bin_op with Fixpoint and
> "match ... in..." like the listn_un_op definition ..........) *)
>
>      Parameter bin_op : nat -> nat -> nat.
>      Definition listn_bin_op :
>           forall (n:nat), listn n -> listn n -> listn n.
>      Proof.
>        induction n as [|n hyp_rec_n]; intros l1 l2. exact niln.
>        inversion l1 as [|nn a1 tl1]; inversion l2 as [|nnn a2 tl2]; subst.
>        exact (consn n (bin_op a1 a2) (hyp_rec_n tl1 tl2)).
>      Defined.
>
>      Lemma ith_of_listn_bin_op :
>      forall i n l1 l2 res1 res2,
>      (ith n l1 i res1) -> (ith n l2 i res2) ->
>      (ith n (listn_bin_op (S n) l1 l2) i (bin_op res1 res2)).
>      Proof.
>        induction i; intros.
>        inversion H; inversion H0; simpl; subst.
>         ???? ..........
>
> --------------------------------------------------------
> 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
>


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Attachment: vectors.v
Description: Binary data