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).
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.
This is one case where ssreflect views do help:
From Coq Require Import ssreflect.
Variable (P Q : Prop).
Axiom u : (P -> Q) -> (~Q -> ~P).
Lemma test (H : P -> Q) : False.
Proof. move/u in H. Abort.
apply u in H does also work, however it is too smart for its own good and does too much.
If I wanted to transform H in place I would go with @ejgallego's answer, since SSReflect is now (starting from Coq 8.7.0) a part of standard Coq, but here is another option:
Ltac dumb_apply_in f H := generalize (f H); clear H; intros H.
Tactic Notation "dumb" "apply" constr(f) "in" hyp(H) := dumb_apply_in f H.
A simple test:
Variable (P Q : Prop).
Axiom u : (P -> Q) -> (~Q -> ~P).
Lemma test (H : P -> Q) : False.
Proof. dumb apply u in H. Abort.
