coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting terms in the conclusion

From: Benjamin GREGOIRE <Benjamin.Gregoire AT inria.fr>
To: Romain Janvier <Romain.Janvier AT imag.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Rewriting terms in the conclusion
Date: Wed, 11 Dec 2002 17:06:03 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Romain Janvier wrote:

Is there a tactic that can automaticly transforme a goal the same way
that "inversion" does with the hypothesys as (Pair A x)=(Pair A B)
giving x=B.

For example if I have (Pair A x)=(Pair A B) in my goal, can I
automaticly obtain x=B as my new goal?

Replace x with B;Trivial.

And if it's possible, can I do the same with a goal as:
(EX x| (Pair A x)=(Pair A B))
And obtain:
(EX x| x=B)
?

I don't thing so.

Exists B;Trivial.

solve your goal.

Benjamin Gregoire

[Coq-Club] Rewriting terms in the conclusion, Romain Janvier
- Re: [Coq-Club] Rewriting terms in the conclusion, Benjamin GREGOIRE
  - Re: [Coq-Club] Rewriting terms in the conclusion, Pierre Courtieu