recursive rw

Stream: general

[Bernd Losert]

Say I have ¬ (∃ (U ∈ f) (V ∈ g), U ∩ V = ∅) and I want to apply rw not_exists recursively to it. How do I do this?

[Patrick Stevens]

Does repeat { rw not_exists, } do what you want?

[Patrick Stevens]

(Actually iterate { rw not_exists, } may be better, and it also lets you specify an n)

[Bernd Losert]

No, it does not seem to work.

[Yaël Dillies]

Why do you get this in the first place? Did you use by_contra instead of by_contra'?

[Yaël Dillies]

simp_rw not_exists

[Bernd Losert]

That worked. Nice.

[Yaël Dillies]

The problem with repeat { rw not_exists } is that rw does not look under binders, and ∃ is a binder, so it will only rewrite the first one.

[Bernd Losert]

I got it from using iff.not on filter.inf_eq_bot_iff.

[Patrick Johnson]

tactic#push_neg

[Bernd Losert]

That's even better.

[Kyle Miller]

Yaël Dillies said:

rw does not look under binders

A reminder that rw does look under binders, it just can't rewrite subexpressions that contain local variables. simp can do it because it knows about funext.

[Yaël Dillies]

Sorry, never know how to put it best!

[Kyle Miller]

"can't look under binders" is a good meme, so it's too bad it's inaccurate.