Search code examples
coqcoq-tactic

Rewrite hypothesis in Coq, keeping implication

I'm doing a Coq proof. I have P -> Q as a hypothesis, and (P -> Q) -> (~Q -> ~P) as a lemma. How can I transform the hypothesis into ~Q -> ~P?

When I try to apply it, I just spawn new subgoals, which isn't helpful.

Put another way, I wish to start with:

P : Prop
Q : Prop
H : P -> Q

and end up with

P : Prop
Q : Prop
H : ~Q -> ~P

given the lemma above - i.e. (P -> Q) -> (~Q -> ~P).

Solution

  • This is not as elegant as just an apply, but you can use pose proof (lemma _ _ H) as H0, where lemma is the name of your lemma. This will add another hypothesis with the correct type to the context, with the name H0.