Zulip Chat Archive

Stream: new members

Topic: rw has trouble pattern matching under quantifiers


view this post on Zulip 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.

view this post on Zulip Reid Barton (May 17 2020 at 12:35):

rw never works under binders, unfortunately.

view this post on Zulip Keefer Rowan (May 17 2020 at 12:38):

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 12:41):

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 12:41):

There's also simp only [h]


Last updated: May 13 2021 at 05:21 UTC