coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,the term (Lem1 y0) as type "exists x: Z, x = func1 (y0)", so you can destruct it to extract
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 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
- [Coq-Club] Introduce existing variable, Michael
- Re: [Coq-Club] Introduce existing variable, Thomas Braibant
- Re: [Coq-Club] Introduce existing variable, Vincent Siles
- <Possible follow-ups>
- Re: Re: [Coq-Club] Introduce existing variable, Michael
Archive powered by MhonArc 2.6.16.