Why can't `rw` rewrite under binders?

Stream: general

[Kevin Buzzard]

Right now we have the silly situation where I explain to mathematicians what rw does, and then they try it when they're using finite sums or whatever, and it doesn't work and you get an inscrurible error, and then I have to tell them that rw doesn't work under binders and you have to use simp_rw instead.

Why can't we just make rw work under binders, e.g. by replacing it with simp_rw?

[Michael Stoll]

rw works in some cases where simp_rw doesn't (when it has to create side goals, which simp does not).

[Michael Stoll]

(Sitting on a train from Munich to Berlin, with a number of your compatriots that want to watch the final :smile: )

[Kevin Buzzard]

Then why can't we "just fix rw so that it works under binders"? All I'm saying is that from a naive usability perspective this just looks totally weird. Maybe I'm being too naive.

[Marcus Rossel]

This is just me guessing, but my impression of the rw tactic has been that it's supposed to be simple and efficient, which mean's that the mechanism it uses for rewriting is also simple (just using the recursor of Eq?). Rewriting under binders requires more sophisticated mechanisms like function extensionality, which in turn requires congruence lemmas, which gets complicated once you have dependent functions. So I think that's why that kind of rewriting is only available in the more complicated tactics like simp.
But would be interesting to hear the reasons from the people who actually know.

[Ralf Stephan]

If rw is so fast then you can automatically try if it works, else use simp_rw?

[Peter Nelson]

There is the annoyance that simp_rw is less ‘surgical’ - what if you only want to apply it exactly once to something inside a binder?

[Riccardo Brasca]

The following works, showing that simp_rw is able to use functional extensionality, something we probably don't want for a basic tactic like rw.

import Mathlib

example (A B : Type) (f g : A → B) (h : ∀ a, f a = g a) : f = g := by
  show (fun a => f a) = fun a => g a
  simp_rw [h]

[Riccardo Brasca]

In particular this simp_rw is impossible to obtain without Quot.sound and propext

[Riccardo Brasca]

Having said that, I agree that it would be nice if import Mathlib could make rw more powerful.

[Michael Rothgang]

How difficult would it be to make rw detect "I'm asked to rewrite under binders" and provide an error "sorry Dave, I can't do that; use simp_rw instead"?

[Yaël Dillies]

@Jovan Gerbscheid has a version of rewrite working under binders

[Kevin Buzzard]

Yes my point is that it's confusing for beginners. It would be nice if the error message said something less confusing than "I can't find the pattern which you can see is visibly there"

[Jovan Gerbscheid]

Yes, making rw work under binders is indeed possible, but the algorithm is a bit more complicated than the current rw. The tricky thing is that the metavariables in the rewrite pattern need to be allowed to depend on the bound variables (which have to be introduced as free variables locally, after those metavariables have already been introduced).

The proof term requires an extra funext for each bound variable that appears in the rewritten expression, so this doesn't make a big impact on the proof complexity.

It would probably be hard to convince the core developpers to change the behaviour of rw. On the other hand, making a change to rw that works under import Mathlib could also confuse people. I imagine that option as making a tactic brw (bound rewriting), which is run automatically if rw fails, and only rewrites at expressions containing bound variables.

[Jovan Gerbscheid]

Michael Rothgang said:

How difficult would it be to make rw detect "I'm asked to rewrite under binders" and provide an error "sorry Dave, I can't do that; use simp_rw instead"?

If you can detect unification with bound variables, then I'd say you may as well go all the way and support rewriting them.

[Jovan Gerbscheid]

Riccardo Brasca said:

simp_rw is able to use functional extensionality, something we probably don't want for a basic tactic like rw.

Why wouldn't you want rw to use funext?

[Riccardo Brasca]

Personally I don't have anything against it, but those axioms aren't even in core, aren't they?

[Jovan Gerbscheid]

Marcus Rossel said:

Rewriting under binders requires more sophisticated mechanisms like function extensionality, which in turn requires congruence lemmas, which gets complicated once you have dependent functions.

I didn't need any congruence lemmas for rewriting bound variables.

[Eric Wieser]

Peter Nelson said:

what if you only want to apply it exactly once to something inside a binder?

I thought you could use singlePass := true for this, but it seems not to always help:

import Mathlib

example (x : ℕ) : (1 + 2) + (1 + 3) = x := by
  simp_rw (config := {singlePass := true}) [add_comm 1 _] -- still does both

[Henrik Böving]

Riccardo Brasca said:

Personally I don't have anything against it, but those axioms aren't even in core, aren't they?

funext is in core, otherwise simp could not work under binders.

[Eric Wieser]

Riccardo Brasca said:

Personally I don't have anything against it, but those axioms aren't even in core, aren't they?

Given core forces Classical.choice upon us when splitting ifs, I doubt anyone cares about funext (aka, propext and Quotient.sound) being used in other core tactics

[Riccardo Brasca]

Ah ok, I didn't think about that

[Marcus Rossel]

Jovan Gerbscheid said:

I didn't need any congruence lemmas for rewriting bound variables.

:thinking: How did you do it?

[Yaël Dillies]

The "congruence lemmas" are generated on the fly. If you want to rewrite a = b in ⨆ n, a + n = ⨆ n, b + n, Jovan's tactic first shows (fun n ↦ a + n) = fun n ↦ b + n then rewrites with that

[Marcus Rossel]

@Yaël Dillies Which tactic is "Jovan's tactic" (/where does it live)?

[Jovan Gerbscheid]

To do it without congruence lemmas, you can beta expand to turn your rewrite into a rewrite without bound variables, if you want the rewrite ⨆ n, a + n = ⨆ n, n + a,
my tactic first shows a + n = n + a. Then by funext, it shows that fun n => a + n = fun n => n + a. Then you can do the usual thing to show that ⨆ n, (fun n => a + n) n = ⨆ n, (fun n => n + a) n,

[Jovan Gerbscheid]

I have an ordered/directed rewrite tactic, and a normal rewrite tactic that rewrite in a given position (unlike rw which figures out the position itself). The ordered rewrite tactic does use specific congruence lemmas. To find the right rewrite congruence lemma, I used type class search to find it.

[Jovan Gerbscheid]

Here's where the rewrite and ordered rewrite tactics live. I wrote them 1 year ago. However they don't work in Lean out of the box, as we were representing the proofstate in a specific custom way.

[Kyle Miller]

This "expression abstraction" trick is what generalize_proofs does to pull proofs out from under binders. In some ways that's easier to handle though since you don't have to worry about "motive not type correct" due to proof irrelevance (with a small proviso due to Acc.rec reduction I suppose...)

[Kyle Miller]

Something I've been wondering is if we can compute a motive for a rewrite in a friendly way, where there's an automated algorithm that can recursively typecheck the motive, replacing subexpressions that it decides are to blame.

There'd be no "motive not type correct" with such an algorithm, at the cost of people wondering why certain rewrites don't seem to be possible.