coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Induction and tuple destruction

chronological Thread

From: David Pichardie <david.pichardie AT irisa.fr>
To: Peter Hawkins <hawkinsp AT cs.stanford.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Induction and tuple destruction
Date: Tue, 30 Jan 2007 09:37:23 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Here is my proposition, based on "generalize".

Lemma foo_lem2: forall a1 b1 a2 b2, foo (a1,b1) (a2,b2)� ->

(a1 <= a2)%nat.

Proof.

� intros a1 b1 a2 b2 H.

� change (fst (a1,b1) <= fst (a2,b2)).

� induction H; simpl in *; omega.

Qed.

Hope this helps,

It seems the induction tactic didn't generate the hypotheses (s =
(a1,b1)) and (s = (a2,b2)). What's happening here, and how can I fix
it? I'm using Coq 8.1gamma.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

David Pichardie

Junior research scientist

INRIA Rennes (IRISA) - projet Lande

Campus de Beaulieu

35042 Rennes, Cedex

France

Phone: (+33) 2 99 84 74 04

Fax: (+33) 2 99 84 71 71

[Coq-Club]Induction and tuple destruction, Peter Hawkins
- Re: [Coq-Club]Induction and tuple destruction, Adam Chlipala
- Re: [Coq-Club]Induction and tuple destruction, Jean-Marc Notin
- Re: [Coq-Club]Induction and tuple destruction, David Pichardie