Lean4
/-- Given `tr := t*r` `sr := s*r` `tEqs : t = s`, return a proof for `tr = sr`
We use `a*b` to denote an AC application. That is, `(a*b)*(c*a)` is the term `a*a*b*c`. -/
def mkACSimpProof (tr t s r sr : ACApps) (tEqs : DelayedExpr) : MetaM DelayedExpr := do
if tr == t then
return tEqs
else if tr == sr then
let some tre := tr.toExpr |
failure
DelayedExpr.ofExpr <$> mkEqRefl tre
else
let .apps op _ := tr |
failure
let some re := r.toExpr |
failure
let some te := t.toExpr |
failure
let some se := s.toExpr |
failure
let some tre := tr.toExpr |
failure
let some sre := sr.toExpr |
failure
let opr := op.app re
let rt := mkApp2 op re te
let rs := mkApp2 op re se
let rtEqrs := DelayedExpr.congrArg opr tEqs
let trEqrt ← mkACProof tre rt
let rsEqsr ← mkACProof rs sre
return .eqTrans (.eqTrans trEqrt rtEqrs) rsEqsr
