Lean4
/-- If `thm` can be used to rewrite `e`, return the rewrite. -/
def checkRewrite (thm e : Expr) (symm : Bool) : MetaM (Option Rewrite) := do
withTraceNodeBefore `rw?? (return m! "rewriting {e} by {(if symm then "← " else "")}{thm}")
(do
let (mvars, binderInfos, eqn) ← forallMetaTelescope (← inferType thm)
let some (lhs, rhs) := eqOrIff? eqn |
return none
let (lhs, rhs) := if symm then (rhs, lhs) else (lhs, rhs)
let unifies ← withTraceNodeBefore `rw?? (return m! "unifying {e } =?= {lhs}") (withReducible (isDefEq lhs e))
unless unifies do
return none
let lhs ← instantiateMVars lhs
if lhs.toHeadIndex != e.toHeadIndex || lhs.headNumArgs != e.headNumArgs then
return none
synthAppInstances `rw?? default mvars binderInfos false false
let mut extraGoals := #[]
for mvar in mvars, bi in binderInfos do
unless ← mvar.mvarId!.isAssigned do
extraGoals := extraGoals.push (mvar.mvarId!, bi)
let replacement ← instantiateMVars rhs
let stringLength := (← ppExpr replacement).pretty.length
let makesNewMVars := (replacement.findMVar? fun mvarId => mvars.any (·.mvarId! == mvarId)).isSome
let proof ← instantiateMVars (mkAppN thm mvars)
return some { symm, proof, replacement, stringLength, extraGoals, makesNewMVars })
