coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fr�d�ric Gava <frederic.gava AT wanadoo.fr>
- To: <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Re: Problem with length of list
- Date: Fri, 23 Jan 2004 11:10:03 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear users,
For the first Lemma, I just forget to siomplify my
sub-goals...
just do:
Lemma put_tmp2: (T:Set)(l1,l2:(list Z->(option T)))(l:(list
Z->(option
T)))(i,j:Z)
(Zlength (Z->(option T)) (put_tmp T l1 i l))=(Zlength (Z->(option T))(put_tmp T l2 j l)). Intros T l.
NewInduction l;Simpl; Intros; Auto.
Rewrite (IHl l1 l2 `i+1` `j+1`); Auto.
Qed
Sorry for this stupid question but I do not
have the proof for my second function (the Double Induction tactics does not
work here).
best regards,
Frédéric Gava
|
- [Coq-Club] Re: Problem with length of list, Frédéric Gava
Archive powered by MhonArc 2.6.16.