Applications have implicit arguments. Thus, two terms that may look identical when pretty-printed can be structurally different. For example, @id (Id Nat) x and @id Nat x are structurally different but are both pretty-printed as id x. Moreover, these two terms are definitionally equal since Id Nat reduces to Nat. This may create situations that are counterintuitive to our users. Furthermore, several tactics (e.g., omega) need to collect unique atoms in a goal. One simple approach is to maintain a list of atoms found so far, and whenever a new atom is discovered, perform a linear scan to test whether it is definitionally equal to a previously found one. However, this method is too costly, even if the definitional equality test were inexpensive.

This module aims to efficiently identify terms that are structurally different, definitionally equal, and structurally equal when we disregard implicit arguments like @id (Id Nat) x and @id Nat x. The procedure is straightforward. For each atom, we create a hash that ignores all implicit information. Thus the hash for terms are equal @id (Id Nat) x and @id Nat x. To preserve any pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while computing the hash code, we employ unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from hash to lists of terms, where each list contains terms sharing the same hash but not definitionally equal. We posit that these lists will be small in practice.

structure Lean.Meta.Canonicalizer.ExprVisited : Type

Auxiliary structure for creating a pointer-equality.

• e : Lean.Expr

instance Lean.Meta.Canonicalizer.instInhabitedExprVisited : Inhabited Lean.Meta.Canonicalizer.ExprVisited

unsafe instance Lean.Meta.Canonicalizer.instBEqExprVisited : BEq Lean.Meta.Canonicalizer.ExprVisited

unsafe instance Lean.Meta.Canonicalizer.instHashableExprVisited : Hashable Lean.Meta.Canonicalizer.ExprVisited

structure Lean.Meta.Canonicalizer.State : Type

State for the CanonM monad.

• cache : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64

  Mapping from Expr to hash.

• keyToExprs : Std.HashMap UInt64 (List Lean.Expr)

  Given a hashcode k and keyToExprs.find? h = some es, we have that all es have hashcode k, and are not definitionally equal modulo the transparency setting used.

instance Lean.Meta.Canonicalizer.instInhabitedState : Inhabited Lean.Meta.Canonicalizer.State

Equations

• Lean.Meta.Canonicalizer.instInhabitedState = { default := { cache := Std.HashMap.Raw.empty, keyToExprs := ∅ } }

@[reducible, inline]

abbrev Lean.Meta.Canonicalizer.CanonM (α : Type) : Type

Equations

• Lean.Meta.CanonM = ReaderT Lean.Meta.TransparencyMode (StateRefT' IO.RealWorld Lean.Meta.Canonicalizer.State Lean.MetaM)

def Lean.Meta.Canonicalizer.CanonM.run' {α : Type} (x : Lean.Meta.CanonM α) (transparency : Lean.Meta.TransparencyMode := Lean.Meta.TransparencyMode.instances) (s : Lean.Meta.Canonicalizer.State := { cache := Std.HashMap.Raw.empty, keyToExprs := ∅ }) : Lean.MetaM α

The definitionally equality tests are performed using the given transparency mode. We claim TransparencyMode.instances is a good setting for most applications.

Equations

• x.run' transparency s = (x transparency).run' s

def Lean.Meta.Canonicalizer.CanonM.run {α : Type} (x : Lean.Meta.CanonM α) (transparency : Lean.Meta.TransparencyMode := Lean.Meta.TransparencyMode.instances) (s : Lean.Meta.Canonicalizer.State := { cache := Std.HashMap.Raw.empty, keyToExprs := ∅ }) : Lean.MetaM (α × Lean.Meta.Canonicalizer.State)

Equations

• x.run transparency s = (x transparency).run s

def Lean.Meta.Canonicalizer.canon (e : Lean.Expr) : Lean.Meta.CanonM Lean.Expr

"Canonicalize" the given expression.

Equations

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