feat: change_matching ... with tactic

[kmill]

This PR implements the change_matching p with r tactic, which replaces each p in the target with r if p and r are definitionally equal. This is like rewrite [show p = r by rfl], but the replacement does not depend on their being a type-correct motive. The tactic is comparable to the Lean 3 change p with r tactic.

Closes #5116

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d1a99d8d45a3460f9150997201345aadc398ab19 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-09 18:51:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d553d63694414f95e89fd328a032702bd32a4a4 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-17 03:44:12)

[nomeata]

This feels similar to the equals conv tactic. Is there a way to use this similarity for a more consistent syntax?

Also, will there be change .. to .. by .., for when the proof isn't just rfl? I see rw [show a = t by tac] a lot, and it looks very clumsy.

Or am I derailing this, if this is less about rewriting and more about changing defeq terms?

[kmill]

@nomeata This one's just for defeq replacement. If it weren't for that, it would be like using pattern p <;> equals t => rfl.

Now's a good time to think about whether this Lean 3 era syntax could be improved, but I haven't thought of anything better. Maybe change p => r? It seems like there ought to be a defeq version of conv for precise navigation and unfolding/replacement...

[nomeata]

Maybe change p => r

Not sure, => is often a tactic herald (case, conv, tactic).

As we discuss this I wonder if a better UX design would be to have similar tactics for the defeq and the rewriting case, and they differ in their suffix. A user likely has a certain aim (goal should be X), and that's what's on their mind first. So they write change X and if it holds definitionally, then great! If not they'll get a suitable error message and can continue with by to prove the equation using a tactic (or maybe using to give a term?).

So maybe same with change p to e? Maybe equals t could have the by optional?

(All not fully throught through, at this time of week :-))

[nomeata]

Oh, and I keep writing change p to t rather than with, which somehow sounds unnatural to me. Is that just me? Or is this maybe a kludge to avoid new keywords?

[kmill]

@nomeata change with is a bit unnatural, but it's understandable. Normally you'd say "change to" or "replace with". Yes, it's a keyword kludge — I think every Lean 3 tactic used only "at"/"using"/"with"/"generalizing" clauses.

change by is interesting, though it's incompatible with how this change with tactic works. I suppose change with by could go through the process of checking the motive for type correctness and performing the rewrite when there's this by clause (change with computes a motive, but there's no need to check it for type correctness). For just change by, Mathlib has convert_to, which creates side goals when things aren't defeq (after applying zero or more congruence lemmas), which covers that use case I think.

[nomeata]

Do we have a strong reason to stick to what we had in lean 3 or can we polish it a bit. For example these sound better to me

• change p to e
• replace p with e
• replace p = e (slight, but neat abuse of notation)

All of these could support an optional proof with by, the last even with :=.

I'm not sure if change p to e and change p to e by tac are too incompatible. Sure, from an implementation point of view theory are different tactics, but both user intention, and the effect on the goal are very compatible, so it seems plausible to present them to the user as variants of the same idea?

And if we had that I think there is room for change by as well. The congruence applying class of functions is in my mind a separate and more complex and less predictable thing. If I have a + b as a goal, then change to b + a by … is a reasonable natural step where the user probably does not want congruence to be applied. In fact I almost always when using convert have to look up how to limit it (using 3, right - odd syntax again) because it often does too much. So it seems to make sense to offer something more basic, more predictable.

(I snuck in a to here, but probably that's not an improvement over the existing change b + a, although the missing preposition has bothered me a bit before - after all change e doesn't actually change e.)

[kmill]

I'm not attached to change with, other than the convenience of not needing to add any new keywords, and other than my own convenience to be able to close this issue that was assigned to me :-)

I wanted to say that change with should have the same head keyword as change, but maybe it would be ok to have a different keyword. Unfortunately though replace is taken. I don't think we should consider renaming the change tactic itself — that would be some unnecessary breakage of code and teaching material. (The = idea doesn't work since it's common to use change when the goal is an equality.)

Regarding the by variants, these are just completely different tactics, so I'm not sure it's worth discussing it here on this PR, though of course it's worth making sure there are syntax variations available. (Note that convert_to defaults to doing just one level of congruence, so it's not too unpredictable.)

[nomeata]

What do you think of non-keywords keywords here (nonReservedSymbol)? Will that work well and give us some syntactic breathing room, or is that a bad idea?

[digama0]

It doesn't work as is, because the non-reserved symbol follows an expression here, and it will mix up the pseudo-keyword with an application to a similarly named identifier. You might be able to get it to parse as desired using notFollowedBy?

[kmill]

I'd like to avoid non-reserved keywords — I find them to feel a bit hacky (though please feel free to experiment to see if it can work well here). What do you think about change_matching p with r @nomeata ? I also tried change p for r, but term-for gets in the way. One more syntax I considered is change p := r or change_matching p := r.

[kmill]

Started a Zulip discussion