Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: Problem with length of list

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Problem with length of list


chronological Thread 
  • 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
 



Archive powered by MhonArc 2.6.16.

Top of Page