Lean4
/-- Transform an equality between 2-morphisms into the equality between their normalizations. -/
def normalForm (ρ : Type) [Context ρ] [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)]
[MonadNormalExpr (CoherenceM ρ)] [MkEval (CoherenceM ρ)] [MkMor₂ (CoherenceM ρ)] [MonadMor₂ (CoherenceM ρ)]
(nm : Name) (mvarId : MVarId) : MetaM (List MVarId) := do
mvarId.withContext do
let e ← instantiateMVars <| ← mvarId.getType
withTraceNode nm (fun _ => return m! "normalize: {e}") do
let some (_, e₁, e₂) := (← whnfR <| ← instantiateMVars <| e).eq? |
throwError "{nm}_nf requires an equality goal"
let ctx : ρ ← mkContext e₁
CoherenceM.run (ctx := ctx) do
let e₁' ← MkMor₂.ofExpr e₁
let e₂' ← MkMor₂.ofExpr e₂
let e₁'' ← eval nm e₁'
let e₂'' ← eval nm e₂'
let H ← mkAppM ``mk_eq #[e₁, e₂, e₁''.expr.e.e, e₂''.expr.e.e, e₁''.proof, e₂''.proof]
mvarId.apply H
