A canonicalizer module for the grind tactic. The canonicalizer defined in Meta/Canonicalizer.lean is not suitable for the grind tactic. It was designed for tactics such as omega, where the goal is to detect when two structurally different atoms are definitionally equal.

The grind tactic, on the other hand, uses congruence closure. Moreover, types, type formers, proofs, and instances are considered supporting elements and are not factored into congruence detection.

This module minimizes the number of isDefEq checks by comparing two terms a and b only if they instances, types, or type formers and are the i-th arguments of two different f-applications. This approach is sufficient for the congruence closure procedure used by the grind tactic.

To further optimize isDefEq checks, instances are compared using TransparencyMode.instances, which reduces the number of constants that need to be unfolded. If diagnostics are enabled, instances are compared using the default transparency mode too for sanity checking, and discrepancies are reported. Types and type formers are always checked using default transparency.

Remark: The canonicalizer minimizes issues with non-canonical instances and structurally different but definitionally equal types, but it does not solve all problems. For example, consider a situation where we have (a : BitVec n) and (b : BitVec m), along with instances inst1 n : Add (BitVec n) and inst2 m : Add (BitVec m) where inst1 and inst2 are structurally different. Now consider the terms a + a and b + b. After canonicalization, the two additions will still use structurally different (and definitionally different) instances: inst1 n and inst2 m. Furthermore, grind will not be able to infer that HEq (a + a) (b + b) even if we add the assumptions n = m and HEq a b.

structure Lean.Meta.Grind.Canon.State : Type

• argMap : Lean.PHashMap (Lean.Expr × Nat) (List Lean.Expr)
• canon : Lean.PHashMap Lean.Expr Lean.Expr
• proofCanon : Lean.PHashMap Lean.Expr Lean.Expr

instance Lean.Meta.Grind.Canon.instInhabitedState : Inhabited Lean.Meta.Grind.Canon.State

Equations

• Lean.Meta.Grind.Canon.instInhabitedState = { default := { argMap := default, canon := default, proofCanon := default } }

def Lean.Meta.Grind.Canon.canonElemCore (f : Lean.Expr) (i : Nat) (e : Lean.Expr) (isInst : Bool) : StateT Lean.Meta.Grind.Canon.State Lean.MetaM Lean.Expr

Helper function for canonicalizing e occurring as the ith argument of an f-application. isInst is true if e is an type class instance.

Recall that we use TransparencyMode.instances for checking whether two instances are definitionally equal or not. Thus, if diagnostics are enabled, we also check them using TransparencyMode.default. If the result is different we report to the user.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Canon.canonType (f : Lean.Expr) (i : Nat) (e : Lean.Expr) : StateT Lean.Meta.Grind.Canon.State Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Grind.Canon.canonType f i e = Lean.Meta.withDefault (Lean.Meta.Grind.Canon.canonElemCore f i e false)

@[reducible, inline]

abbrev Lean.Meta.Grind.Canon.canonInst (f : Lean.Expr) (i : Nat) (e : Lean.Expr) : StateT Lean.Meta.Grind.Canon.State Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Grind.Canon.canonInst f i e = Lean.Meta.withReducibleAndInstances (Lean.Meta.Grind.Canon.canonElemCore f i e true)

instance Lean.Meta.Grind.Canon.instInhabitedShouldCanonResult : Inhabited Lean.Meta.Grind.Canon.ShouldCanonResult✝

Equations

• Lean.Meta.Grind.Canon.instInhabitedShouldCanonResult = { default := Lean.Meta.Grind.Canon.ShouldCanonResult.canonType✝ }

def Lean.Meta.Grind.Canon.shouldCanon (pinfos : Array Lean.Meta.ParamInfo) (i : Nat) (arg : Lean.Expr) : Lean.MetaM Lean.Meta.Grind.Canon.ShouldCanonResult✝

See comments at ShouldCanonResult.

Equations

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

unsafe def Lean.Meta.Grind.Canon.canonImpl (e : Lean.Expr) : StateT Lean.Meta.Grind.Canon.State Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Grind.Canon.canonImpl e = (Lean.Meta.Grind.Canon.canonImpl.visit e).run' Lean.mkPtrMap

unsafe def Lean.Meta.Grind.Canon.canonImpl.visit (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.PtrMap Lean.Expr Lean.Expr) (StateT Lean.Meta.Grind.Canon.State Lean.MetaM) Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.letE declName type value body nonDep) = pure (Lean.Expr.letE declName type value body nonDep)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.forallE binderName binderType body binderInfo) = pure (Lean.Expr.forallE binderName binderType body binderInfo)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.lam binderName binderType body binderInfo) = pure (Lean.Expr.lam binderName binderType body binderInfo)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.const declName us) = pure (Lean.Expr.const declName us)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.lit a) = pure (Lean.Expr.lit a)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.mvar mvarId) = pure (Lean.Expr.mvar mvarId)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.sort u) = pure (Lean.Expr.sort u)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.fvar fvarId) = pure (Lean.Expr.fvar fvarId)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.proj typeName idx struct) = pure (Lean.Expr.proj typeName idx struct)
• Lean.Meta.Grind.Canon.canonImpl.visit (Lean.Expr.mdata data expr) = pure (Lean.Expr.mdata data expr)

def Lean.Meta.Grind.Canon.canon (e : Lean.Expr) : StateT Lean.Meta.Grind.Canon.State Lean.MetaM Lean.Expr

Canonicalizes nested types, type formers, and instances in e.

Equations

• Lean.Meta.Grind.Canon.canon e = Lean.Meta.Grind.Canon.canon.unsafe_impl_1 e