Point-and-click tactics

Stream: general

[Anand Rao Tadipatri]

By default, Lean's rw tactic unfolds all occurrences of a pattern, which can be a bit limiting in proofs that require targeted rewrites. Here is a demonstration of a point-and-click widget that allows users to select a sub-expression to generate a rw tactic call with a configuration targeting that location. The source code for the tactic is available here: https://github.com/Human-Oriented-ATP/lean-tactics/blob/main/MotivatedMoves/ForMathlib/Rewrite.lean.

rw_demo.gif

The folder also contains a point-and-click widget for definitional unfolding, where the location of the target is specified via patterns and occurrences.

unfold_demo.gif

Future work might include targeted rewriting with library results using @Jovan Gerbscheid's DiscrTrees (a crude preview of which is shown below), as well as targeted function application.

lib_rw_demo.gif

Would a PR of these tactics to Std or Mathlib be welcome?

[Eric Wieser]

I would guess that Std is a good target for these

[Eric Wieser]

This maybe raises that occss should be part of the at clause? It feels like it only makes sense per-target, not globally

[Patrick Massot]

Again I think it would be nice to unify this with the existing framework used in Mathlib for conv?, congrm? and the calc widget. I don't mind getting rid of my framework if yours is better, but I don't think we should have both in parallel unless they really have different use cases (which doesn't seem to be true).

[Anand Rao Tadipatri]

I agree -- I will modify the UI part of the code to use mkSelectionPanelRPC.

[Anand Rao Tadipatri]

Eric Wieser said:

This maybe raises that occss should be part of the at clause? It feels like it only makes sense per-target, not globally

At the moment, the tactic is designed to target a single location, so it is usually a single argument for both occs and at, but I agree that it would be nice to target multiple locations simultaneously (and to couple the occs with the at as a way to allow that). Alternatively, when multiple locations involving several local hypotheses are selected, a sequence of tactics is pasted into the editor (one for each hypothesis involved).

In the future, I would like to also have syntax for targeting values of let hypotheses and allowing users to select all occurrences (perhaps through a checkbox in the infoview).

[Kevin Buzzard]

Can I have this in NNG I wonder?

[Eric Wieser]

Patrick's concerns look reasonable; but it seems that the unfold' tactic (which is new, right?) is orthogonal to them; could you PR the non-interactive version to Std?

[Scott Morrison]

@Anand Rao Tadipatri, in your first example (5+6=6+5) you end up inserting a tactic that is overkill: it has both Nat.comm 5 6 (i.e. arguments provided) and an occs parameter.

Either would suffice. Would it be possible to give more succinct output?

A few things you could do:

• find the specialization, and then see if now rewrites in a single location (using kabstract)
• try out both the specialized rewrite, and the occs rewrite. If only one works, use that, otherwise use whichever is shorted textually?

[Scott Morrison]

It would also be lovely if the infoview highlighted the possible subexpressions (which you could access via kabstract).

[Scott Morrison]

But these feature requests are much less important than having a path to integrating this into Std + Mathlib.

[Scott Morrison]

(This is really nice!)

[Anand Rao Tadipatri]

Kevin Buzzard said:

Can I have this in NNG I wonder?

I find that I'm unable to select sub-expressions by shift-clicking in the NNG (at least on my browser), but in principle it should be possible. (I suspect that this part of the Lean4Game source code controls the shift-click behaviour.)

[Anand Rao Tadipatri]

@Scott Morrison Thanks for the detailed feedback -- I would like to shorten the tactic call in the editor to something more readable as well. I realised that the specialisation is in fact necessary in certain situations, since kabstract instantiates meta-variables in the query during unification, which can affect sub-sequent matches. Here is an example that illustrates this:

example : 1 + 2 = 3 + 4 := by
  rw (config := { occs := .pos [2] }) [Nat.add_comm] -- error
  -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  --   1 + 2
  -- 1 + 2 = 3 + 4

The second occurrence of the pattern ?n + ?m in the target is 3 + 4, so one would expect the tactic call to rewrite at that location, but it instead throws an error since the first occurrence of the pattern (1 + 2) instantiates the meta-variables and prevents the second match from happening.

[Scott Morrison]

@Anand Rao Tadipatri, see my open Lean 4 PR trying to improve this behaviour: lean4#2539 :-)

[Anand Rao Tadipatri]

In that case, I agree that it is perhaps best to drop the specialisation and operate entirely using occs (or the other way, using occs sparingly). With the second approach, I'm only worried that this might add additional time to creating the rewrite tactic call that gets pasted into the editor, which can have a cumulative effect in a tactic like rw? which generates multiple rw calls. Could this instead be a tactic code action in the editor that deletes the config to rw when it is redundant?

[Anand Rao Tadipatri]

Scott Morrison said:

It would also be lovely if the infoview highlighted the possible subexpressions (which you could access via kabstract).

Thank you for this suggestion, this is a feature that I would really like the tactic to have!

[Anand Rao Tadipatri]

(deleted)

[Anand Rao Tadipatri]

I have opened a pull request std4#417 for the unfold' tactic, according to Eric's suggestion.

[Anand Rao Tadipatri]

I have been working on @Eric Wieser's suggestion of allowing each hypothesis to maintain a separate list of occurrences (the code is at std4#417). The idiomatic Lean way of specifying targets is through syntax of the form at h h' ... ⊢, which I generalised to syntax of the form at h ‹h' (occs := 1)› ‹h'' (occs := 1) in body› ⊢, which allows referring to specific occurrences in the types of hypotheses or the bodies of local let declarations.

I would appreciate feedback on this design choice. The syntax has one sore point remaining -- occurrences in the target cannot use the syntax ‹⊢ (occs := 1)›, since then ⊢ gets confused for an identifier; my temporary solution is to use differently styled parentheses (<> instead of ‹›) to refer to occurrences in the target (which I find unsatisfactory).

[Yaël Dillies]

Hmm, interesting. I would have thought that the more pressing thing was not to allow rewriting with occurrences at different hypotheses, but rather rewriting with occurrences using several lemmas.

[Scott Morrison]

Both of these seem rather unnecessary: you can do these things already, just needing multiple rw statements. Unless there was some performance problem, I think this would just result in extra syntax to learn.