Highlighting a subexpression when using rw tactic..

Stream: general

[Seth Chaiken]

I really enjoyed Will's talk and got helpful ideas about how to approach using VSCode/Lean more effectively. I just returned to reading Mathematics in Lean. I suggest here a UI interface feature where we could type in the rw tactic, highlight a sub-expression in the goal (shown in Infoview), then specify a theorem, and the system will supply or suggest the arguments to apply the theorem for rewriting the highlighted sub-expression. This might be better than the current behavior in which the system highlights the sub-expression it chooses. Similar features for other tactics would be good too.

[Richard Copley]

Perhaps such a feature could work by first inserting a conv and the appropriate navigation commands, then using rw?. In that case it would be necessary first to implement rw?as a conv tactic.

[Anand Rao Tadipatri]

A prototype of such a tactic can be seen here (CC: @Jovan Gerbscheid ): https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Point.26Click.20library.20rewrite.20tactic/near/427677844

[Jovan Gerbscheid]

That thread is really long, but essentially I've made a tactic which does what you ask, called rw?? (I still need to make it work without a pre-computed cache of the library). The tactic lets you click on a subexpression, and then suggests all possible rewrites to do in that position. You can then select one of these, and the relevant rw tactic will be pasted into the editor