Why does `rw` not rewrite inside quantifiers?

Stream: mathlib4

[Gareth Ma]

As title, why doesn't rw rewrite inside quantifiers? Is it because of performance issues or what? I know simp_rw does but the issue seems counterintuitive for beginners.

[Kyle Miller]

rw and simp (which is what simp_rw is itself using) use completely different techniques to rewrite. The rw tactic does permit rewriting under quantifiers, but the rewritten term just can't reference any of the bound variables. Both rw and simp can do things that the other cannot; simp only can rewrite one thing at a time, which can be a problem when there are complicated dependent types, but simp is able to reliable rewrite under binders because it can use funext to navigate into such subexpressions.

I'd tried explaining it here, but there are other explanations scattered around Zulip as well. (Probably searching for "rw" and "binders" will help.)

[Patrick Massot]

Kyle, it would be nice to gather all those explanations to a blog post or documentation page. I'm sure it would save you time in the long run.

[Gareth Ma]

I suggest making a FAQ page at https://leanprover-community.github.io/ that you can just point to (perhaps even with a zulip command)

[Bhavik Mehta]

Maybe we can adapt @Eric Rodriguez 's older FAQ page

[Riccardo Brasca]

Also, functional extensionality doesn't hold in Lean's type theory (one needs quot.sound to prove it), so rewriting under a lambda requires an additional axiom, and sometimes people want to pay attention to that.

[Riccardo Brasca]

Of course this is irrelevant in "standard mathematics".