simplifyACCore — Mathlib

Lean4
/-- Given `e := lhs * r` and `H : lhs = rhs`, return `rhs * r` and the proof of `e = rhs * r`. -/
def simplifyACCore (e lhs rhs : ACApps) (H : DelayedExpr) : CCM (ACApps × DelayedExpr) := do
  guard (lhs.isSubset e)
  if e == lhs then
    return (rhs, H)
  else
    let .apps op _ := e |
      failure
    let newArgs := e.diff lhs
    let r : ACApps := if newArgs.isEmpty then default else .mkApps op newArgs
    let newArgs := ACApps.append op rhs newArgs
    let newE := ACApps.mkApps op newArgs
    let some true := (← get).opInfo[op]? |
      failure
    let newPr ← mkACSimpProof e lhs rhs r newE H
    return (newE, newPr)
Похожие утверждения