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 new abstracted atom by erasing all implicit information. We refer to this abstracted atom as a 'key.' For the two terms mentioned, the key would be @id _ x, where _ denotes a placeholder for a dummy term. To preserve any pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while constructing the key, we employ unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from keys to lists of terms, where each list contains terms sharing the same key 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 mapping from Expr to Key. We use this mapping to ensure we preserve the dag-structure of input expressions.

• e : Lean.Expr

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

Equations

• Lean.Meta.Canonicalizer.instInhabitedExprVisited = { default := { e := default } }

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

Equations

• Lean.Meta.Canonicalizer.instBEqExprVisited = { beq := fun (a b : Lean.Meta.Canonicalizer.ExprVisited) => ptrAddrUnsafe a == ptrAddrUnsafe b }

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

Equations

• Lean.Meta.Canonicalizer.instHashableExprVisited = { hash := fun (a : Lean.Meta.Canonicalizer.ExprVisited) => (ptrAddrUnsafe a).toUInt64 }

@[reducible, inline]

abbrev Lean.Meta.Canonicalizer.Key : Type

Equations

• Lean.Meta.Canonicalizer.Key = Lean.Meta.Canonicalizer.ExprVisited

structure Lean.Meta.Canonicalizer.State : Type

State for the CanonM monad.

• keys : ShareCommon.State Lean.ShareCommon.objectFactory

  "Set" of all keys created so far. This is a hash-consing helper structure available in Lean.

• cache : Lean.HashMapImp Lean.Meta.Canonicalizer.ExprVisited Lean.Meta.Canonicalizer.Key

  Mapping from Expr to Key. See comment at ExprVisited.

• keyToExprs : Lean.HashMapImp Lean.Meta.Canonicalizer.Key (List Lean.Expr)

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

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

Equations

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

@[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 : optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances) : 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 = (x transparency).run' { keys := ShareCommon.State.mk Lean.ShareCommon.objectFactory, cache := Lean.mkHashMapImp, keyToExprs := Lean.mkHashMapImp }

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.