rewrite at SubExpr.Pos

Stream: lean4

[Marcus Rossel]

If I have a goal : Expr, t : Term and p : SubExpr.Pos, is there some way to perform a rewrite on goal at position p using t? So in pseudo-code rw (pos := p) [t].

[Anand Rao Tadipatri]

@Marcus Rossel I have been working on something along these lines over here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Point-and-click.20tactics/near/405360088. The selected SubExpr.Pos is converted to a pattern and occurrence which is then pasted into the editor. Functions for going from the SubExpr.Pos to the occurrence in the expression are in the source code linked to in the message.

[Marcus Rossel]

Oh, great! So I guess I could use findRewriteOccurrence and then use the result to do:

rw (config := { occs := ...}) [t]

Is that right?

[Anand Rao Tadipatri]

Yes, that's right. You may need to specialize t because of the way Lean's kabstract (which is used for rw) works.

The function that generates the final tactic call as a string is rewriteTacticCall.

Here is a modified version that suits your situation (this assumes that the rewrite is happening in the goal):

def rewriteTacticCall' (goal : Expr) (p : SubExpr.Pos) (thm : Expr) (symm : Bool) : MetaM String := do
  let (occurrence, pattern) ← findRewriteOccurrence thm symm p goal
  let cfg : Rewrite.Config := { occs := .pos [occurrence] }
  let arg : String := Format.pretty <| ← ppExpr pattern -- the `pattern` is the `thm` specialized to the selected position
  return s!"rw (config := {cfg}) [{if symm then "← " else "" ++ arg}]"

[Marcus Rossel]

Anand Rao Tadipatri said:

You may need to specialize t because of the way Lean's kabstract (which is used for rw) works.

Why is this actually necessary? I would have thought that this call to isDefEq would match the metavariables in pattern to the corresponding subexpressions in ← SubExpr.patternAt position root. Or is this not the case?

[Anand Rao Tadipatri]

Yes, that call to isDefEq would ensure that the meta-variables are instantiated with the correct values. I was earlier referring to the term that ends up in the final tactic call -- if t is Nat.add_comm, then it may need to be specialized down to something like Nat.add_comm 3 4 for it to work as intended (the example below shows a case where just Nat.add_comm fails).

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

But this is a behaviour that may soon be fixed: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Point-and-click.20tactics/near/405517524.

[Marcus Rossel]

Oh perfect, that's exactly an error I've been running into which I didn't understand :innocent:
Thanks so much for you detailed explanations!

[Anand Rao Tadipatri]

I'm glad to help!

[Marcus Rossel]

PSA: I tried using the #2539 toolchain, and it didn't fix the aforementioned problem. For example, I still get:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Nat.add a b + c
a b c : Nat
⊢ a + b + c = c + b + a

[Marcus Rossel]

Interestingly, removing the ← reduce (skipTypes := false) (skipProofs := false) in findRewriteOccurrence solved the problem for me.

[Anand Rao Tadipatri]

Thanks, I will look into this. I suppose that with the new kabstract, it would be possible to avoid the pattern from findRewriteOccurrences entirely in the rewriteTacticCall' function:

def rewriteTacticCall' (goal : Expr) (p : SubExpr.Pos) (thm : Expr) (symm : Bool) : MetaM String := do
  let (occurrence, _) ← findRewriteOccurrence thm symm p goal
  let cfg : Rewrite.Config := { occs := .pos [occurrence] }
  let arg : String := Format.pretty <| ← ppExpr thm
  return s!"rw (config := {cfg}) [{if symm then "← " else "" ++ arg}]"