What to call the Lean 3 `change ... with ...` tactic?

Stream: lean4

[Kyle Miller]

Recall that the Lean 3 tactic change p with r would search for all subexpressions matching p in the target and replace them with r. It is sort of like rw [show p = r by rfl], but it avoids any sort of "motive not type correct" error. The replacement r has to be defeq to p.

Now that we're in Lean 4, we could have a fresh start with the syntax. The change p with r syntax isn't so bad, but it's also not so illuminating what it will be, plus it should be change p to r or change p for r to be more grammatical.

Some constraints are that it would be good to make sure the keyword used is a keyword, and it would be nice to avoid introducing a new keyword.

Some ideas:

1. change_matching p with r — still uses with not-so-grammatically, but at least we see the word matching
2. change p := r — no need for a new keyword, but doesn't evoke changing all occurrences of p.
3. Scrap it, create a dconv tactic mode, and have it be dconv in p => change r (or equivalently dconv => pattern p <;> change r). Sort of appealing, though it is a good amount of work, and it also is more limited with how it handles locations (like change p with r at *), at least if it handles locations the way conv itself does.
4. Scrap it, create a drw tactic that is to rw as dsimp is to simp. You would write drw [p = r]. We could make it so that drw [h] allows h to either be a proof or a proposition, allowing drw to accept rw lemmas where the LHS is defeq to the RHS (the proof in this case would be discarded).

I'm sort of leaning toward 4 here. However, elaboration works better with a change ... with ... tactic (i.e., you might be able to avoid some type ascriptions), since it can figure out the type of p from whatever it matches in the target expression and use that to elaborate of r, though maybe the flexibility of drw outweights that minor inconvenience.

[Yakov Pechersky]

change p => r?

[Joachim Breitner]

I like the direction of drw. There is a variant where the keyword is still rw and either it just always does that when the lemma is a rfl lemma, or there is some marker on the argument that says that it should do rfl rewriting. This is related to https://github.com/leanprover/lean4/issues/6033

[Joachim Breitner]

Yakov Pechersky said:

change p => r?

Also quite nice, thanks for the suggestion! In particular neat when this means that change r is roughly the same as change _ => r.

[Kyle Miller]

@Joachim Breitner I thought you weren't keen on that suggestion earlier :wink:

[Kyle Miller]

I'm not sure I see the connection to lean4#6033, other than that if rw can doing matching under binders then so should drw

[Joachim Breitner]

Kyle Miller said:

Joachim Breitner I thought you weren't keen on that suggestion earlier :wink:

fair point :-D. I had that objection again now, and the reminded myself of fun _ => _, where there isn't a tactic afterwards :-).

The connection to that RFC is the desire that rw should just do all forms the rewriting maybe? Rather than having a myriad of rewriting like tactics?

[Edward van de Meent]

if we're really set on with, replace would be a grammatical name...

[Edward van de Meent]

that is, unless i'm pulling a foreign

[Kyle Miller]

"replace p with r" is grammatical, but replace x := v is a pre-existing tactic

[Edward van de Meent]

what does that tactic do?

[Joachim Breitner]

Acts like have, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:

f : α → β
h : α
⊢ goal

Then after replace h := f h the state will be:

f : α → β
h : β
⊢ goal

whereas have h := f h would result in:

f : α → β
h† : α
h : β
⊢ goal

This can be used to simulate the specialize and apply at tactics of Coq.

[Joachim Breitner]

At a high level, my not completely worked out thinking is that our tactics would look a bit differently if they were designed altogether, and from a user’s point of view, rather than their differing implementation.

For example, when rewriting, we need to know what to rewrite, what to rewrite to, and how to rewrite it (e.g. by rfl, by a rewrite lemma, or by an explicit proof). Often some of these are implicit – with change the “what” is implicitly the whole goal, with rw the “what” is the rule’s lhs and the “what to” is the pattern; with the tactic discussed here the what and what to is explicit, but it only works for one of the “hows”.

I’d wager that users tend to think first about what they want to achieve (e.g. rewrite p to r; strawman suggestions), and only then want to think about the how? That suggests that they should be able to write that, then get feedback from the system (e.g. indicate that it doesn't hold definitionally and a proof is necessary ) and then continue with the justification (e.g. using p_eq_r, or by simp […])

Or maybe the user knows the how first, e.g. know they want to apply p_eq_r, and they write something that leaves the “what” implicit (e.g. rewrite using p_eq_r), and then notice that the inferred “what” wasn’t quite the right one. Wouldn’t it be nice if they wouldn’t have to use a completely different tactic now, but could just add more information (rewrite p using p_eq_r).

In the end there could be a single flexible and tactic that subsumed a whole set of rewriting and changing related tactics (rewrite, simp_rw, change, change with , maybe also unfold) , and and is hopefully easier and more consistent to use.

I’m not saying that this vision is easily achievable, specially due to backwards compat considerations (but not only), and it shouldn’t block incremental improvements like this one. But it’s may a vision worth keeping in mind?

[Kyle Miller]

I think there's still a place for more precise tactics, but I do like the vision of a tactic that makes a rewrite happen using multiple strategies, and it's something I've been thinking about too.

I mentioned it in that PR thread, but convert_to is a tactic that defers the "how" and uses multiple strategies to try to prove the rewrite. It's just missing a change ... with-like interface. It's also missing Eq.rec-type strategies. By default it uses using 1, which seems to work as a heuristic, but having it do using 0 (or having it choose a "reasonable" depth automatically) is plausible.

[Joachim Breitner]

I don't want the tactic to be less precise, though! Same expressiveness, just a unified, compositional, consistent interface, with convenient and ergonomic defaults to the same features (or a superset thereof), including optional knobs for extra control (e.g. I could imagine such a tactic to behave like change if the lemma given is a rfl lemma, but have a way to use the Eq.rec-strategy explicitly)

[Kyle Miller]

By "precision" I mean regarding the proof strategy, not in what's being rewritten, and it seems that one possible disagreement here is whether 'compositional' means between different tactics or whether there should be a featureful main rewrite tactic that can be configured with a compositional syntax (I'm reminded of the LOOP macro in Lisp, which is compositional in the second way but not the first).

[Joachim Breitner]

Good points. As user I don't care too much of if it's a single tactic with optional fields, or a clever combination of tactics and tactic combinators. But it's probably easier with a main tactic, especially the “user says what they want, system gives feedback, user refines the tactic line” goal.

[Joachim Breitner]

Consider the at $loc syntax. To a user, this might actually feel like a tactic combinator or modifier, since it works (mostly) consistently across different tactics. You learn it once, apply it elsewhere, and maybe even naturally discover it's use with other tactics. I'd consider this compositional for these purposes, even though the actual implementation isn't (every tactic implements it again, of course using helpers).

[Joachim Breitner]

So if you want all the variant of this envisioned tactic could be their own syntax declarations with separate elaborators, and thus technically separate tactics, and still together give the UX of a single tactic.