The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

I am frequently in the situation like

 

H: P->Q

---------

False

 

For some P and Q such that (P->Q)->False.

 

Now I would like to work on the hypothesis P. In my case this would be most convenient using a sequence of eapply tactics. The most convenient way I found to do this is

 

assert (P) as HP.

<many eapply to get P>.

specialize (H HP).

(inversion of H (which is Q now) leads to a contradiction)

 

Using evar and specialize with these evars also somehow works, but is much less convenient (I need about 10 evars for the case, and for half of them the type also needs to be an evar). eapply can resolve all this nicely.

 

But I don’t like asserting P, because cut and paste assert proofs are usually not very readable / maintainable. Ok, I can write an Ltac to assert the premises of a given hypothesis or use “lapply H. intros HP. all: swap 1 2.”, … but still I don’t like it. I would find it most natural to work backwards incrementally on P with something like “especialize”, a variant of specialize allowing holes and working with evars like eapply. Is there some direct way (without assert) to work on P as if it would be the current goal? Note: eapply in H would go forward from Q, not backward from P.

 

Are there any other tactics than specialize to work on P?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928