coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] mathematical proof language and tactic rewrite

From: Saulo Araujo <saulo2 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] mathematical proof language and tactic rewrite
Date: Sat, 21 Feb 2015 08:21:57 -0300

Hi Michel,

I am not sure if I understood your question completely but maybe

assert (H12variant := variant).

rewrite H11 in H12variant

is what you are looking for.

Regards,

Saulo

On Sat, Feb 21, 2015 at 6:35 AM, Michel Levy <michel.levy1948 AT gmail.com> wrote:

I wanted to write a proof only in the mathematical proof language (Reference Manual chapter 11).
But in my proof, I used the tactic (not in this language) : rewrite H11 in H12.
I would have preferred to add a NEW hypothesis H12variant , copy of the H12 obtained by "rewrite H11 in H12", WITHOUT modification of H12.
How to do that ?
-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy 

[Coq-Club] mathematical proof language and tactic rewrite, Michel Levy, 02/21/2015
- Re: [Coq-Club] mathematical proof language and tactic rewrite, Saulo Araujo, 02/21/2015
  - Re: [Coq-Club] mathematical proof language and tactic rewrite, Michel Levy, 02/21/2015