rw has trouble pattern matching under quantifiers

Stream: new members

[Keefer Rowan]

I've noticed that rw has trouble pattern matching under quantifiers. E.g. in this proof:

theorem mwe {P Q : nat → Prop} : ∀ (x : nat), ¬ (P x → Q x):=
begin
    --rw classical.not_implies_iff,
    sorry,
end

the rewrite fails where: theorem not_implies_iff {P Q : Prop} : ¬ (P → Q) ↔ P ∧ ¬ Q.

My guess is the it isn't interpreting P x and Q x as Props but as predicates, so it can't pattern match. But is there a way to get it to match? Perhaps I should just be using some fancy logic tactic?

I know to get that rw we could first just intro x, but there are cases where this would be a bit annoying to do. It feels like there should be a better way to do this.

[Reid Barton]

rw never works under binders, unfortunately.

[Keefer Rowan]

Ok thanks, good to know at least I'm not being stupid.

[Kevin Buzzard]

Isn't there some beefed up rewrite tactic which does do this?

[Kevin Buzzard]

There's also simp only [h]