Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Introduce existing variable

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Introduce existing variable


chronological Thread 
  • From: Vincent Siles <vsiles AT lix.polytechnique.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Introduce existing variable
  • Date: Mon, 19 Jul 2010 11:09:03 +0200

Hi Michael,

On 19/07/2010 11:04, Michael wrote:
Hello,

I've got a Lemma, stating that for every y of myType there's a corresponding
x:Z

Lem1:
   forall (y: myType),
   exists x : Z,
   (x = func1(y)),
Admitted.

Now in my proof, I've got some variables of myType in a formula, which I would
like to be replaced, e.g.:

func1(y0) * 3<= func1(y0) * 4 + 3
the term (Lem1 y0) as type "exists x: Z, x = func1 (y0)", so you can destruct it to extract
the corresponding x and the rewriting hypothesis you need (by using destruct, or elim, or whatever).

destruct (Lem1 y0) as (x0 & h0).
rewrite <- h0.

This should create the rewriting hypothesis you need, and rewrite func1(y0) with x0 in your goal.
You can do rewrite 2! <- h0 to rewrite both occurences at once.

Vincent




Archive powered by MhonArc 2.6.16.

Top of Page