Tactic by manipulating Expr

Stream: lean4

[Tomas Skrivan]

If I have a function Expr -> MetaM (Expr × Expr) that turns an expression to an another expression and also provide a proof that they are equal. How do I turn this into a tactic that rewrites the goal?

Also, what if I have only Expr -> MetaM Expr but can also generate tactic proof of that the output is equal to the input. How can I make a tactic to rewrite the goal?

I had a rough idea how to do it in lean3 but in lean4 I'm stomped.

[Jakob von Raumer]

First use that function in a function MVarId -> MetaM MVarId which returns a new MVar with the new goal, assigns the input MVar with the result of substituting with the equality and assigning the substituted MVar with the new MVar.
Then you need to define a Tactic which calls that function and sets the main goal to its output.

[Tomas Skrivan]

Thanks! It pointed me to the right direction.

Actually, the function more or less exists already Lean.Meta.replaceTargetEq :)

I still need to figure out what is the best way to create the equality proof(its Expr representation) if I know the tactic proof for it.

[Chris B]

There are some examples in the current version of mathlib4's normNum, particularly here. https://github.com/leanprover-community/mathlib4/blob/7ac569847b94980d3d668ae6079131f5cd2fe559/Mathlib/Tactic/NormNum.lean#L104

[Tomas Skrivan]

I think, I'm on the right track, but running into problems with universes(something I do not really understand)

I'm trying to write a simple tactic that replaces the current goal X with two new goals X = id X and id X. The first goal X = id X should be solvable by simp but I'm getting an error incorrect number of universe levels id

import Lean
import Lean.Meta.Basic
import Lean.Elab.Tactic.Basic

open Lean
open Lean.Meta
open Lean.Elab.Tactic

syntax (name := mytactic) "mytactic" : tactic

def mytacticCore (mvarId : MVarId) : MetaM (List MVarId) :=
  withMVarContext mvarId do
    let tag      ← getMVarTag mvarId
    let target   ← getMVarType mvarId
    let u        ← getLevel target
    let targetNew := (mkApp (mkConst `id) target)
    let mvarNew  ← mkFreshExprSyntheticOpaqueMVar targetNew tag
    let eq       ← mkEq target targetNew
    let eqMvar  ← mkFreshExprSyntheticOpaqueMVar eq tag
    let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqMvar, mvarNew]
    assignExprMVar mvarId val
    return [eqMvar.mvarId!, mvarNew.mvarId!]


@[tactic mytactic] def tacticMytactic : Tactic
| _ => do
          let mainGoal ← getMainGoal
          let todos ← mytacticCore mainGoal
          setGoals todos
          pure ()

theorem test (X : Type) (x : X) : id x = x :=
  by
    mytactic
    simp

[Chris B]

id needs a universe. Without looking too careully at it I would assume you can just use u here:

let targetNew := (mkApp (mkConst `id [u]) target)

[Chris B]

If you print a declaration and it has a little .{u} or something else tacked onto the end, that means it takes one or more (one in this case) universe parameters in this context.

#print id
-- def id.{u} : {α : Sort u} → α → α := ..

[Tomas Skrivan]

Thanks! Makes sense. I just recalled from "Lean Together 2021: Metaprogramming in Lean 4" that there is mkAppM that deals will all of this for me. So switching two lines to:

    let targetNew ← mkAppM `id #[target]
    let val  ← mkAppM `Eq.mpr #[eqMvar, mvarNew]

Makes it work and I do not have to deal with universes and implicit arguments.

[Chris B]

Nice, that does seem handy.