Targeted rewrite: conv_rw?

[siddhartha-gadgil]

This follows an idea of Scott Morrison, and is for use both directly in Mathlib (potentially) and with LeanAide.

• Instead of matching DiscTree's in all subexpressions, one navigates into lambdas and function applications as in the conv tactic mode.
• The resulting candidates are of the form conv => enter[...] => rw [..]

[0art0]

The built-in Lean type SubExpr may be useful here. A SubExpr is determined by a SubExpr.Pos, which is a type synonym for Nat; however, the function SubExpr.Pos.toArray decodes the Nat to a familiar Array of indices which determine the path along the expression tree.

[0art0]

Closely related to targeted rewriting with conv is this demo from the ProofWidgets repository. A variation of the solveLevel function might be what is required.

[siddhartha-gadgil]

@0art0 Does the widget work under binders, for example with:

example : ∀ x: ℕ, x + 3 = 3 + x := by
  conv =>
    enter [x, 2]
    rw [Nat.add_comm]
  intro _ 
  rfl

If so I agree we should follow that code, with navigating to all positions instead of based on clicks.

[0art0]

Yes, I tested the above example and it does work under binders too.

[siddhartha-gadgil]

@0art0 What is the suggested tactic sequence there? Does it give enter [x, 2] or equivalent?

[0art0]

Yes, it gave enter [x, 1] (as I chose to rewrite the left-hand side).

[siddhartha-gadgil]

That is perfect then. One just has to copy part of the code (excluding widget stuff) and simulate clicking everywhere. Then one can use the code of rw? (maybe not going into sub-expressions).

[0art0]

I will try to tackle this tomorrow.