CODEWITHSUNDEEP
logiccoqproofcoq-tactic
some1fromhell
some1fromhell

Reputation: 135

How to use apply to "extract" a implication in Coq

I'll illustrate using an example.

H : R -> P -> Q

H0 : R

Subgoal:

(Q -> P) \ / (P -> Q)

so my question is how do I extract out (P->Q). I have R already, but when I do 'apply H in H0', it evaluates everything and gives me Q.

Upvotes: 0

Views: 139

Answers (1)

Ptival
Ptival

Reputation: 9447

You can do any of:

specialize (H H0).

to replace H with H: P -> Q, or:

pose proof (H H0) as H1

to introduce H1: P -> Q

You can also go forward:

right. exact (H H0).

Upvotes: 2

Related Questions