## Stream: new members

### Topic: rw has trouble pattern matching under quantifiers

#### Keefer Rowan (May 17 2020 at 12:28):

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 (May 17 2020 at 12:35):

rw never works under binders, unfortunately.

#### Keefer Rowan (May 17 2020 at 12:38):

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

#### Kevin Buzzard (May 17 2020 at 12:41):

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

#### Kevin Buzzard (May 17 2020 at 12:41):

There's also simp only [h]

Last updated: May 13 2021 at 05:21 UTC