simplify an expression in a meta program

Stream: lean4

[Yury G. Kudryashov]

If I have e : Expr, how do I get e' : Expr and h : e = e', where e' is the simplified version of e?

[Alex J. Best]

docs#Lean.Meta.simp gives a docs#Lean.Meta.Simp.Result, which basically contains what you want

[Tomas Skrivan]

Alternatively you can run any conv tactic with this code:

import Lean

open Lean.Parser.Tactic.Conv
open Lean.Elab.Tactic.Conv

open Lean Elab Term Meta

def elabConvRewrite (e : Expr) (stx : TSyntax `conv) : TermElabM (Expr × Expr) := do
  let (rhs, eq) ← mkConvGoalFor e

  let goals ← Tactic.run eq.mvarId! do
    let (lhsNew, proof) ← convert e (Tactic.evalTactic stx)
    updateLhs lhsNew proof
    return ()

  if goals.length = 0 then
    throwError "this is a bug in `elabConvRewrite`"elab

  if goals.length > 1 then
    throwError s!"error in `elabConvRewrite`, unsolved goals {← goals.mapM (fun g => do ppExpr (← g.getType))}"

  (goals.get! 0).refl

  return (← instantiateMVars rhs, ← instantiateMVars eq)

Running simplifier would be elabConvRewrite e (<- `(simp))

[Kyle Miller]

Mathlib has some frontends to simp as well. See for example how the reassoc tactic simplifies a type: https://github.com/leanprover-community/mathlib4/blob/eee126916c924c75dc6b3b43e42c5fc354153fdb/Mathlib/Tactic/CategoryTheory/Reassoc.lean#L49

There are more variations in Mathlib.Lean.Meta.Simp