Type-directed canonicalizer

Canonicalizes expressions by normalizing types and instances. At the top level, it traverses applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance, implicit, or value using shouldCanon. Targeted reductions (projection, match/ite/cond, Nat arithmetic) are applied to all positions; instances are re-synthesized.

Note about types: grind is not built for reasoning about types that are not propositions. We assume that definitionally equal types will be structurally identical after we apply the canonicalizer. We also erase most of the subsingleton markers occurring inside types.

Reductions

It also normalizes expressions using the following reductions. We can view it as a cheap/custom dsimp. We used to reduce only terms inside types, but it restricted important normalizations that were important when, for example, a term had a forward dependency. That is, the term is not directly in a type, but there is a type that depends on it.

• Eta: fun x => f x → f
• Projection: ⟨a, b⟩.1 → a (structure projections, not class projections)
• Match/ite/cond: reduced when discriminant is a constructor or literal
• Nat arithmetic: ground evaluation (2 + 1 → 3) and offset normalization (n.succ + 1 → n + 2)

Note: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring in non type positions, we want to leverage the support in grind for lambda-expressions.

Instance canonicalization

Instances are re-synthesized via synthInstance. The instance type is first normalized using the type-level reductions above, so that OfNat (Fin (2+1)) 0 and OfNat (Fin 3) 0 produce the same canonical instance. Two special cases:

• Decidable instances (Grind.nestedDecidable): the proposition is recursively canonicalized, then the Decidable instance is re-synthesized. If resynthesis fails, the original instance is kept (users often provide these via haveI). A checkDefEqInst guard is required because structurally different Decidable instances are not necessarily definitionally equal.

• Propositional instances (Grind.nestedProof): the proposition is recursively canonicalized, then the proof is re-synthesized. If resynthesis fails, the original proof is kept. No definitional-equality check is needed thanks to proof irrelevance.

In both cases, resynthesis failure is silent — the original instance or proof is kept. Ideally we would report an issue when resynthesis fails inside a type (where structural agreement matters most), but in practice users provide non-synthesizable instances via haveI, and these instances propagate into types through forward dependencies. Reporting failures for such instances produces noise that obscures real issues.

Two caches

The canonicalizer maintains separate caches for type-level and value-level contexts. The same expression may canonicalize differently depending on whether it appears in a type position (where reductions are applied) or a value position (where it is only traversed). Caches are keyed by Expr (structural equality), not pointer equality, because the canonicalizer runs before shareCommon and enters binders using locally nameless representation.

Future work

If needed we should add support for user-defined extensions.

def Lean.Meta.Sym.Canon.isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool

Returns true if shouldCanon pinfos i arg is not .visit. This is a helper function used to implement mbtc.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.canon (e : Expr) : SymM Expr

Canonicalize e by normalizing types, instances, and support arguments. Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions; eta reduction is applied only inside types. Instances are re-synthesized. Runs at reducible transparency.

Equations

• Lean.Meta.Sym.canon e = do let __do_lift ← Lean.getOptions Lean.profileitM Lean.Exception "sym canon" __do_lift (Lean.Meta.withReducible (Lean.Meta.Sym.Canon.canon✝ e { }))