Lean4
/-- Independently simplify both the left-hand side and the right-hand side
of an equality. The equality is allowed to be under binders.
Returns the simplified equality and a proof of it. -/
def simpEq (S : Expr → MetaM Simp.Result) (type pf : Expr) : MetaM (Expr × Expr) := do
forallTelescope type fun fvars type => do
let .app (.app (.app (.const `Eq [u]) α) lhs) rhs := type |
throwError"simpEq expecting Eq"
let ⟨lhs', lhspf?, _⟩ ← S lhs
let ⟨rhs', rhspf?, _⟩ ← S rhs
let mut pf' := mkAppN pf fvars
if let some lhspf := lhspf? then
pf' ← mkEqTrans (← mkEqSymm lhspf) pf'
if let some rhspf := rhspf? then
pf' ← mkEqTrans pf' rhspf
let type' := mkApp3 (mkConst ``Eq [u]) α lhs' rhs'
return (← mkForallFVars fvars type', ← mkLambdaFVars fvars pf')
