Rewrite hypothesis in Coq, keeping implication

Question

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).

Answer 1

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.

Answer 2

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.

Answer 3

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.