rw rewriting multiple subexpressions

Stream: lean4

[Thomas Murrills]

When does rw rewrite multiple subexpressions, and when does it just rewrite a single subexpression? Are there human-predictable rules?

[Thomas Murrills]

(Is it that all equal subexpressions get rewritten together?)

[Yaël Dillies]

It rewrites only one subexpression, but it can rewrite it in multiple locations.

[Yaël Dillies]

Namely, add_zero rewrites a + 0 = b ∧ a + 0 = c to a = b ∧ a = c but a + 0 = c ∧ b + 0 = c to a = c ∧ b + 0 = c.

[Thomas Murrills]

Ah, got it, thanks! :) (Maybe we should put this behavior in the docstring if anyone gets the chance—and preferably copy the rewrite docstring over to rw as well.)

[Kyle Miller]

One of the keywords here is that it does the "kabstract" algorithm (docs#Lean.Meta.kabstract). It tries unifying the LHS of the rw lemma with every plausible subexpression in the target ("plausible" means that the subexpression has the same docs#Lean.Expr.toHeadIndex), and every subexpression that matches gets rewritten.

Key here is that unification has the side effect of solving for metavariables, which causes the rw lemma to become specialized, so essentially the first match sets which subexpression it looks for in the rest of the expression. (And why metavariables? That's how you instantiate a lemma for isDefEq checks. In particular, rewrite uses docs#Lean.Meta.forallMetaTelescopeReducing on the type of the rw lemma and then uses mkAppN to feed these to the lemma itself.)

[Scott Morrison]

Note also there's an open PR which will change the behaviour, "feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences" lean4#2539, although it has stalled for a while.