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 are 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.

def Lean.Meta.Grind.Canon.canonElemCore (parent f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr

Helper function for canonicalizing e occurring as the ith argument of an f-application. If useIsDefEqBounded is true, we try isDefEqBounded before returning false

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Canon.canonType (parent f : Expr) (i : Nat) (e : Expr) : GoalM Expr

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Canon.canonInst (parent f : Expr) (i : Nat) (e : Expr) : GoalM Expr

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Canon.canonImplicit (parent f : Expr) (i : Nat) (e : Expr) : GoalM Expr

Equations

• Lean.Meta.Grind.Canon.canonImplicit parent f i e = Lean.Meta.withReducible (Lean.Meta.Grind.Canon.canonElemCore parent 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✝ }

instance Lean.Meta.Grind.Canon.instReprShouldCanonResult : Repr Lean.Meta.Grind.Canon.ShouldCanonResult✝

Equations

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

def Lean.Meta.Grind.Canon.shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : 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 : Expr) : GoalM 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 : Expr) : StateRefT' IO.RealWorld (PtrMap Expr Expr) GoalM Expr

Equations

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

def Lean.Meta.Grind.canon (e : Expr) : GoalM Expr

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

Equations

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