Datatypes for cc

Some of the data structures here are used in multiple parts of the tactic. We split them into their own file.

TODO

This file is ported from C++ code, so many declarations lack documents.

def Mathlib.Tactic.CC.isValue (e : Lean.Expr) : Bool

Return true if e represents a constant value (numeral, character, or string).

Equations

• Mathlib.Tactic.CC.isValue e = (e.int?.isSome || e.isCharLit || e.isStringLit)

def Mathlib.Tactic.CC.isInterpretedValue (e : Lean.Expr) : Lean.MetaM Bool

Return true if e represents a value (nat/int numeral, character, or string).

In addition to the conditions in Mathlib.Tactic.CC.isValue, this also checks that kernel computation can compare the values for equality.

Equations

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

def Mathlib.Tactic.CC.liftFromEq (R : Lean.Name) (H : Lean.Expr) : Lean.MetaM Lean.Expr

Given a reflexive relation R, and a proof H : a = b, build a proof for R a b

Equations

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

def Mathlib.Tactic.CC.instOrdExpr_mathlib : Ord Lean.Expr

Ordering on Expr.

Equations

• Mathlib.Tactic.CC.instOrdExpr_mathlib = { compare := fun (a b : Lean.Expr) => bif a.lt b then Ordering.lt else bif b.eqv a then Ordering.eq else Ordering.gt }

@[reducible, inline]

abbrev Mathlib.Tactic.CC.RBExprMap (α : Type u) : Type u

Red-black maps whose keys are Exprs.

TODO: the choice between RBMap and HashMap is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashMap could be more optimal.

Equations

• Mathlib.Tactic.CC.RBExprMap α = Batteries.RBMap Lean.Expr α compare

@[reducible, inline]

abbrev Mathlib.Tactic.CC.RBExprSet : Type

Red-black sets of Exprs.

TODO: the choice between RBSet and HashSet is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashSet could be more optimal.

Equations

• Mathlib.Tactic.CC.RBExprSet = Batteries.RBSet Lean.Expr compare

structure Mathlib.Tactic.CC.CCCongrTheoremextends Lean.Meta.CongrTheorem : Type

CongrTheorems equipped with additional infos used by congruence closure modules.

• type : Lean.Expr
• proof : Lean.Expr
• argKinds : Array Lean.Meta.CongrArgKind
• heqResult : Bool

  If heqResult is true, then lemma is based on heterogeneous equality and the conclusion is a heterogeneous equality.

• hcongrTheorem : Bool

  If hcongrTheorem is true, then lemma was created using mkHCongrWithArity.

def Mathlib.Tactic.CC.mkCCHCongrWithArity (fn : Lean.Expr) (nargs : Nat) : Lean.MetaM (Option Mathlib.Tactic.CC.CCCongrTheorem)

Automatically generated congruence lemma based on heterogeneous equality.

This returns an annotated version of the result from Lean.Meta.mkHCongrWithArity.

Equations

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

structure Mathlib.Tactic.CC.CCCongrTheoremKey : Type

Keys used to find corresponding CCCongrTheorems.

• fn : Lean.Expr

  The function of the given CCCongrTheorem.

• nargs : Nat

  The number of arguments of fn.

instance Mathlib.Tactic.CC.instBEqCCCongrTheoremKey : BEq Mathlib.Tactic.CC.CCCongrTheoremKey

Equations

• Mathlib.Tactic.CC.instBEqCCCongrTheoremKey = { beq := Mathlib.Tactic.CC.beqCCCongrTheoremKey✝ }

instance Mathlib.Tactic.CC.instHashableCCCongrTheoremKey : Hashable Mathlib.Tactic.CC.CCCongrTheoremKey

Equations

• Mathlib.Tactic.CC.instHashableCCCongrTheoremKey = { hash := Mathlib.Tactic.CC.hashCCCongrTheoremKey✝ }

@[reducible, inline]

abbrev Mathlib.Tactic.CC.CCCongrTheoremCache : Type

Caches used to find corresponding CCCongrTheorems.

Equations

• Mathlib.Tactic.CC.CCCongrTheoremCache = Std.HashMap Mathlib.Tactic.CC.CCCongrTheoremKey (Option Mathlib.Tactic.CC.CCCongrTheorem)

structure Mathlib.Tactic.CC.CCConfig : Type

Configs used in congruence closure modules.

• ignoreInstances : Bool

  If true, congruence closure will treat implicit instance arguments as constants.

  This means that setting ignoreInstances := false will fail to unify two definitionally equal instances of the same class.

• ac : Bool

  If true, congruence closure modulo Associativity and Commutativity.

• hoFns : Option (List Lean.Name)

  If hoFns is some fns, then full (and more expensive) support for higher-order functions is only considered for the functions in fns and local functions. The performance overhead is described in the paper "Congruence Closure in Intensional Type Theory". If hoFns is none, then full support is provided for all constants.

• em : Bool

  If true, then use excluded middle

• values : Bool

  If true, we treat values as atomic symbols

instance Mathlib.Tactic.CC.instInhabitedCCConfig : Inhabited Mathlib.Tactic.CC.CCConfig

Equations

• Mathlib.Tactic.CC.instInhabitedCCConfig = { default := { ignoreInstances := default, ac := default, hoFns := default, em := default, values := default } }

inductive Mathlib.Tactic.CC.ACApps : Type

An ACApps represents either just an Expr or applications of an associative and commutative binary operator.

• ofExpr (e : Lean.Expr) : Mathlib.Tactic.CC.ACApps

  An ACApps of just an Expr.

• apps (op : Lean.Expr) (args : Array Lean.Expr) : Mathlib.Tactic.CC.ACApps

  An ACApps of applications of a binary operator. args are assumed to be sorted.

  See also ACApps.mkApps if args are not yet sorted.

instance Mathlib.Tactic.CC.instInhabitedACApps : Inhabited Mathlib.Tactic.CC.ACApps

Equations

• Mathlib.Tactic.CC.instInhabitedACApps = { default := ↑default }

instance Mathlib.Tactic.CC.instBEqACApps : BEq Mathlib.Tactic.CC.ACApps

Equations

• Mathlib.Tactic.CC.instBEqACApps = { beq := Mathlib.Tactic.CC.beqACApps✝ }

instance Mathlib.Tactic.CC.instCoeExprACApps : Coe Lean.Expr Mathlib.Tactic.CC.ACApps

Equations

• Mathlib.Tactic.CC.instCoeExprACApps = { coe := Mathlib.Tactic.CC.ACApps.ofExpr }

def Mathlib.Tactic.CC.instOrdACApps : Ord Mathlib.Tactic.CC.ACApps

Ordering on ACApps sorts .ofExpr before .apps, and sorts .apps by function symbol, then by shortlex order.

Equations

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

def Mathlib.Tactic.CC.ACApps.isSubset (e₁ e₂ : Mathlib.Tactic.CC.ACApps) : Bool

Return true iff e₁ is a "subset" of e₂.

Example: The result is true for e₁ := a*a*a*b*d and e₂ := a*a*a*a*b*b*c*d*d. The result is also true for e₁ := a and e₂ := a*a*a*b*c.

Equations

• One or more equations did not get rendered due to their size.
• (↑a).isSubset ↑b = (a == b)
• (↑e).isSubset (Mathlib.Tactic.CC.ACApps.apps op args) = args.contains e
• (Mathlib.Tactic.CC.ACApps.apps op args).isSubset ↑e = false

def Mathlib.Tactic.CC.ACApps.diff (e₁ e₂ : Mathlib.Tactic.CC.ACApps) (r : Array Lean.Expr := #[]) : Array Lean.Expr

Appends elements of the set difference e₁ \ e₂ to r. Example: given e₁ := a*a*a*a*b*b*c*d*d*d and e₂ := a*a*a*b*b*d, the result is #[a, c, d, d]

Precondition: e₂.isSubset e₁

Equations

• One or more equations did not get rendered due to their size.
• (↑e₂_2).diff e₂ r = if (e₂ == ↑e₂_2) = true then r else r.push e₂_2

def Mathlib.Tactic.CC.ACApps.append (op : Lean.Expr) (e : Mathlib.Tactic.CC.ACApps) (r : Array Lean.Expr := #[]) : Array Lean.Expr

Appends arguments of e to r.

Equations

• Mathlib.Tactic.CC.ACApps.append op (Mathlib.Tactic.CC.ACApps.apps op₂ args₂) r = if (op₂ == op) = true then r ++ args₂ else r
• Mathlib.Tactic.CC.ACApps.append op (↑e₂_1) r = r.push e₂_1

def Mathlib.Tactic.CC.ACApps.intersection (e₁ e₂ : Mathlib.Tactic.CC.ACApps) (r : Array Lean.Expr := #[]) : Array Lean.Expr

Appends elements in the intersection of e₁ and e₂ to r.

Equations

• One or more equations did not get rendered due to their size.
• e₁.intersection e₂ r = r

def Mathlib.Tactic.CC.ACApps.mkApps (op : Lean.Expr) (args : Array Lean.Expr) : Mathlib.Tactic.CC.ACApps

Sorts args and applies them to ACApps.apps.

Equations

• Mathlib.Tactic.CC.ACApps.mkApps op args = Mathlib.Tactic.CC.ACApps.apps op (args.qsort Lean.Expr.lt)

def Mathlib.Tactic.CC.ACApps.mkFlatApps (op : Lean.Expr) (e₁ e₂ : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.ACApps

Flattens given two ACApps.

Equations

• Mathlib.Tactic.CC.ACApps.mkFlatApps op e₁ e₂ = Mathlib.Tactic.CC.ACApps.mkApps op (Mathlib.Tactic.CC.ACApps.append op e₂ (Mathlib.Tactic.CC.ACApps.append op e₁))

def Mathlib.Tactic.CC.ACApps.toExpr : Mathlib.Tactic.CC.ACApps → Option Lean.Expr

Converts an ACApps to an Expr. This returns none when the empty applications are given.

Equations

• (Mathlib.Tactic.CC.ACApps.apps op { toList := [] }).toExpr = none
• (Mathlib.Tactic.CC.ACApps.apps op { toList := arg₀ :: args }).toExpr = some (List.foldl (fun (e arg : Lean.Expr) => Lean.mkApp2 op e arg) arg₀ args)
• (↑e).toExpr = some e

@[reducible, inline]

abbrev Mathlib.Tactic.CC.RBACAppsMap (α : Type u) : Type u

Red-black maps whose keys are ACAppses.

TODO: the choice between RBMap and HashMap is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashMap could be more optimal.

Equations

• Mathlib.Tactic.CC.RBACAppsMap α = Batteries.RBMap Mathlib.Tactic.CC.ACApps α compare

@[reducible, inline]

abbrev Mathlib.Tactic.CC.RBACAppsSet : Type

Red-black sets of ACAppses.

TODO: the choice between RBSet and HashSet is not obvious: the current version follows the Lean 3 C++ implementation. Once the cc tactic is used a lot in Mathlib, we should profile and see if HashSet could be more optimal.

Equations

• Mathlib.Tactic.CC.RBACAppsSet = Batteries.RBSet Mathlib.Tactic.CC.ACApps compare

inductive Mathlib.Tactic.CC.DelayedExpr : Type

For proof terms generated by AC congruence closure modules, we want a placeholder as an equality proof between given two terms which will be generated by non-AC congruence closure modules later. DelayedExpr represents it using eqProof.

• ofExpr (e : Lean.Expr) : Mathlib.Tactic.CC.DelayedExpr

  A DelayedExpr of just an Expr.

• eqProof (lhs rhs : Lean.Expr) : Mathlib.Tactic.CC.DelayedExpr

  A placeholder as an equality proof between given two terms which will be generated by non-AC congruence closure modules later.

• congrArg (f : Lean.Expr) (h : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to congr_arg.

• congrFun (h : Mathlib.Tactic.CC.DelayedExpr) (a : Mathlib.Tactic.CC.ACApps) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to congr_fun.

• eqSymm (h : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to Eq.symm.

• eqSymmOpt (a₁ a₂ : Mathlib.Tactic.CC.ACApps) (h : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to Eq.symm.

• eqTrans (h₁ h₂ : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to Eq.trans.

• eqTransOpt (a₁ a₂ a₃ : Mathlib.Tactic.CC.ACApps) (h₁ h₂ : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to Eq.trans.

• heqOfEq (h : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to heq_of_eq.

• heqSymm (h : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.DelayedExpr

  Will be applied to HEq.symm.

instance Mathlib.Tactic.CC.instInhabitedDelayedExpr : Inhabited Mathlib.Tactic.CC.DelayedExpr

Equations

• Mathlib.Tactic.CC.instInhabitedDelayedExpr = { default := ↑default }

instance Mathlib.Tactic.CC.instCoeExprDelayedExpr : Coe Lean.Expr Mathlib.Tactic.CC.DelayedExpr

Equations

• Mathlib.Tactic.CC.instCoeExprDelayedExpr = { coe := Mathlib.Tactic.CC.DelayedExpr.ofExpr }

inductive Mathlib.Tactic.CC.EntryExpr : Type

This is used as a proof term in Entrys instead of Expr.

• ofExpr (e : Lean.Expr) : Mathlib.Tactic.CC.EntryExpr

  An EntryExpr of just an Expr.

• congr : Mathlib.Tactic.CC.EntryExpr

  dummy congruence proof, it is just a placeholder.

• eqTrue : Mathlib.Tactic.CC.EntryExpr

  dummy eq_true proof, it is just a placeholder

• refl : Mathlib.Tactic.CC.EntryExpr

  dummy refl proof, it is just a placeholder.

• ofDExpr (e : Mathlib.Tactic.CC.DelayedExpr) : Mathlib.Tactic.CC.EntryExpr

  An EntryExpr of a DelayedExpr.

instance Mathlib.Tactic.CC.instInhabitedEntryExpr : Inhabited Mathlib.Tactic.CC.EntryExpr

Equations

• Mathlib.Tactic.CC.instInhabitedEntryExpr = { default := ↑default }

instance Mathlib.Tactic.CC.instToMessageDataEntryExpr : Lean.ToMessageData Mathlib.Tactic.CC.EntryExpr

Equations

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

instance Mathlib.Tactic.CC.instCoeExprEntryExpr : Coe Lean.Expr Mathlib.Tactic.CC.EntryExpr

Equations

• Mathlib.Tactic.CC.instCoeExprEntryExpr = { coe := Mathlib.Tactic.CC.EntryExpr.ofExpr }

structure Mathlib.Tactic.CC.Entry : Type

Equivalence class data associated with an expression e.

• next : Lean.Expr

  next element in the equivalence class.

• root : Lean.Expr

  root (aka canonical) representative of the equivalence class.

• cgRoot : Lean.Expr

  root of the congruence class, it is meaningless if e is not an application.

• target : Option Lean.Expr

  When e was added to this equivalence class because of an equality (H : e = tgt), then we store tgt at target, and H at proof. Both fields are none if e == root

• proof : Option Mathlib.Tactic.CC.EntryExpr

  When e was added to this equivalence class because of an equality (H : e = tgt), then we store tgt at target, and H at proof. Both fields are none if e == root

• acVar : Option Lean.Expr

  Variable in the AC theory.

• flipped : Bool

  proof has been flipped

• interpreted : Bool

  true if the node should be viewed as an abstract value

• constructor : Bool

  true if head symbol is a constructor

• hasLambdas : Bool

  true if equivalence class contains lambda expressions

• heqProofs : Bool

  heqProofs == true iff some proofs in the equivalence class are based on heterogeneous equality. We represent equality and heterogeneous equality in a single equivalence class.

• fo : Bool

  If fo == true, then the expression associated with this entry is an application, and we are using first-order approximation to encode it. That is, we ignore its partial applications.

• size : Nat

  number of elements in the equivalence class, it is meaningless if e != root

• mt : Nat

  The field mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have occurred in the current branch. It is incremented after each round of heuristic instantiation. The field mt records the last time any proper descendant of this entry was involved in a merge.

instance Mathlib.Tactic.CC.instInhabitedEntry : Inhabited Mathlib.Tactic.CC.Entry

Equations

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

@[reducible, inline]

abbrev Mathlib.Tactic.CC.Entries : Type

Stores equivalence class data associated with an expression e.

Equations

• Mathlib.Tactic.CC.Entries = Mathlib.Tactic.CC.RBExprMap Mathlib.Tactic.CC.Entry

structure Mathlib.Tactic.CC.ACEntry : Type

Equivalence class data associated with an expression e used by AC congruence closure modules.

• idx : Nat

  Natural number associated to an expression.

• RLHSOccs : Mathlib.Tactic.CC.RBACAppsSet

  AC variables that occur on the left hand side of an equality which e occurs as the left hand side of in CCState.acR.

• RRHSOccs : Mathlib.Tactic.CC.RBACAppsSet

  AC variables that occur on the left hand side of an equality which e occurs as the right hand side of in CCState.acR. Don't confuse.

instance Mathlib.Tactic.CC.instInhabitedACEntry : Inhabited Mathlib.Tactic.CC.ACEntry

Equations

• Mathlib.Tactic.CC.instInhabitedACEntry = { default := { idx := default, RLHSOccs := default, RRHSOccs := default } }

def Mathlib.Tactic.CC.ACEntry.ROccs (ent : Mathlib.Tactic.CC.ACEntry) (inLHS : Bool) : Mathlib.Tactic.CC.RBACAppsSet

Returns the occurrences of this entry in either the LHS or RHS.

Equations

• ent.ROccs true = ent.RLHSOccs
• ent.ROccs false = ent.RRHSOccs

structure Mathlib.Tactic.CC.ParentOcc : Type

Used to record when an expression processed by cc occurs in another expression.

• expr : Lean.Expr
• symmTable : Bool

  If symmTable is true, then we should use the symmCongruences, otherwise congruences. Remark: this information is redundant, it can be inferred from expr. We use store it for performance reasons.

@[reducible, inline]

abbrev Mathlib.Tactic.CC.ParentOccSet : Type

Red-black sets of ParentOccs.

Equations

• Mathlib.Tactic.CC.ParentOccSet = Batteries.RBSet Mathlib.Tactic.CC.ParentOcc (Ordering.byKey Mathlib.Tactic.CC.ParentOcc.expr compare)

@[reducible, inline]

abbrev Mathlib.Tactic.CC.Parents : Type

Used to map an expression e to another expression that contains e.

When e is normalized, its parents should also change.

Equations

• Mathlib.Tactic.CC.Parents = Mathlib.Tactic.CC.RBExprMap Mathlib.Tactic.CC.ParentOccSet

inductive Mathlib.Tactic.CC.CongruencesKey : Type

• fo (fn : Lean.Expr) (args : Array Lean.Expr) : Mathlib.Tactic.CC.CongruencesKey

  fn is First-Order: we do not consider all partial applications.

• ho (fn arg : Lean.Expr) : Mathlib.Tactic.CC.CongruencesKey

  fn is Higher-Order.

instance Mathlib.Tactic.CC.instBEqCongruencesKey : BEq Mathlib.Tactic.CC.CongruencesKey

Equations

• Mathlib.Tactic.CC.instBEqCongruencesKey = { beq := Mathlib.Tactic.CC.beqCongruencesKey✝ }

instance Mathlib.Tactic.CC.instHashableCongruencesKey : Hashable Mathlib.Tactic.CC.CongruencesKey

Equations

• Mathlib.Tactic.CC.instHashableCongruencesKey = { hash := Mathlib.Tactic.CC.hashCongruencesKey✝ }

@[reducible, inline]

abbrev Mathlib.Tactic.CC.Congruences : Type

Maps each expression (via mkCongruenceKey) to expressions it might be congruent to.

Equations

• Mathlib.Tactic.CC.Congruences = Std.HashMap Mathlib.Tactic.CC.CongruencesKey (List Lean.Expr)

structure Mathlib.Tactic.CC.SymmCongruencesKey : Type

• h₁ : Lean.Expr
• h₂ : Lean.Expr

instance Mathlib.Tactic.CC.instBEqSymmCongruencesKey : BEq Mathlib.Tactic.CC.SymmCongruencesKey

Equations

• Mathlib.Tactic.CC.instBEqSymmCongruencesKey = { beq := Mathlib.Tactic.CC.beqSymmCongruencesKey✝ }

instance Mathlib.Tactic.CC.instHashableSymmCongruencesKey : Hashable Mathlib.Tactic.CC.SymmCongruencesKey

Equations

• Mathlib.Tactic.CC.instHashableSymmCongruencesKey = { hash := Mathlib.Tactic.CC.hashSymmCongruencesKey✝ }

@[reducible, inline]

abbrev Mathlib.Tactic.CC.SymmCongruences : Type

The symmetric variant of Congruences.

The Name identifies which relation the congruence is considered for. Note that this only works for two-argument relations: ModEq n and ModEq m are considered the same.

Equations

• Mathlib.Tactic.CC.SymmCongruences = Std.HashMap Mathlib.Tactic.CC.SymmCongruencesKey (List (Lean.Expr × Lean.Name))

@[reducible, inline]

abbrev Mathlib.Tactic.CC.SubsingletonReprs : Type

Stores the root representatives of subsingletons.

Equations

• Mathlib.Tactic.CC.SubsingletonReprs = Mathlib.Tactic.CC.RBExprMap Lean.Expr

@[reducible, inline]

abbrev Mathlib.Tactic.CC.InstImplicitReprs : Type

Stores the root representatives of .instImplicit arguments.

Equations

• Mathlib.Tactic.CC.InstImplicitReprs = Mathlib.Tactic.CC.RBExprMap (List Lean.Expr)

@[reducible, inline]

abbrev Mathlib.Tactic.CC.TodoEntry : Type

Equations

• Mathlib.Tactic.CC.TodoEntry = (Lean.Expr × Lean.Expr × Mathlib.Tactic.CC.EntryExpr × Bool)

@[reducible, inline]

abbrev Mathlib.Tactic.CC.ACTodoEntry : Type

Equations

• Mathlib.Tactic.CC.ACTodoEntry = (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr)

structure Mathlib.Tactic.CC.CCStateextends Mathlib.Tactic.CC.CCConfig : Type

Congruence closure state. This may be considered to be a set of expressions and an equivalence class over this set. The equivalence class is generated by the equational rules that are added to the CCState and congruence, that is, if a = b then f(a) = f(b) and so on.

• ignoreInstances : Bool
• ac : Bool
• hoFns : Option (List Lean.Name)
• em : Bool
• values : Bool
• entries : Mathlib.Tactic.CC.Entries

  Maps known expressions to their equivalence class data.

• parents : Mathlib.Tactic.CC.Parents

  Maps an expression e to the expressions e occurs in.

• congruences : Mathlib.Tactic.CC.Congruences

  Maps each expression to a set of expressions it might be congruent to.

• symmCongruences : Mathlib.Tactic.CC.SymmCongruences

  Maps each expression to a set of expressions it might be congruent to, via the symmetrical relation.

• subsingletonReprs : Mathlib.Tactic.CC.SubsingletonReprs

  Stores the root representatives of subsingletons.

• instImplicitReprs : Mathlib.Tactic.CC.InstImplicitReprs

  Records which instances of the same class are defeq.

• frozePartitions : Bool

  The congruence closure module has a mode where the root of each equivalence class is marked as an interpreted/abstract value. Moreover, in this mode proof production is disabled. This capability is useful for heuristic instantiation.

• canOps : Mathlib.Tactic.CC.RBExprMap Lean.Expr

  Mapping from operators occurring in terms and their canonical representation in this module

• opInfo : Mathlib.Tactic.CC.RBExprMap Bool

  Whether the canonical operator is supported by AC.

• acEntries : Mathlib.Tactic.CC.RBExprMap Mathlib.Tactic.CC.ACEntry

  Extra Entry information used by the AC part of the tactic.

• acR : Mathlib.Tactic.CC.RBACAppsMap (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr)

  Records equality between ACApps.

• inconsistent : Bool

  Returns true if the CCState is inconsistent. For example if it had both a = b and a ≠ b in it.

• gmt : Nat

  "Global Modification Time". gmt is a number stored on the CCState, it is compared with the modification time of a cc_entry in e-matching. See CCState.mt.

instance Mathlib.Tactic.CC.instInhabitedCCState : Inhabited Mathlib.Tactic.CC.CCState

Equations

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

def Mathlib.Tactic.CC.CCState.mkEntryCore (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) (interpreted constructor : Bool) : Mathlib.Tactic.CC.CCState

Update the CCState by constructing and inserting a new Entry.

Equations

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

def Mathlib.Tactic.CC.CCState.root (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.Expr

Get the root representative of the given expression.

Equations

• ccs.root e = match Batteries.RBMap.find? ccs.entries e with | some n => n.root | none => e

def Mathlib.Tactic.CC.CCState.next (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.Expr

Get the next element in the equivalence class. Note that if the given Expr e is not in the graph then it will just return e.

Equations

• ccs.next e = match Batteries.RBMap.find? ccs.entries e with | some n => n.next | none => e

def Mathlib.Tactic.CC.CCState.isCgRoot (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Bool

Check if e is the root of the congruence class.

Equations

• ccs.isCgRoot e = match Batteries.RBMap.find? ccs.entries e with | some n => e == n.cgRoot | none => true

def Mathlib.Tactic.CC.CCState.mt (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Nat

"Modification Time". The field mt is used to implement the mod-time optimization introduced by the Simplify theorem prover. The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have occurred in the current branch. It is incremented after each round of heuristic instantiation. The field mt records the last time any proper descendant of this entry was involved in a merge.

Equations

• ccs.mt e = match Batteries.RBMap.find? ccs.entries e with | some n => n.mt | none => ccs.gmt

def Mathlib.Tactic.CC.CCState.inSingletonEqc (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Bool

Is the expression in an equivalence class with only one element (namely, itself)?

Equations

• ccs.inSingletonEqc e = match Batteries.RBMap.find? ccs.entries e with | some it => it.next == e | none => true

def Mathlib.Tactic.CC.CCState.getRoots (ccs : Mathlib.Tactic.CC.CCState) (roots : Array Lean.Expr) (nonsingletonOnly : Bool) : Array Lean.Expr

Append to roots all the roots of equivalence classes in ccs.

If nonsingletonOnly is true, we skip all the singleton equivalence classes.

Equations

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

def Mathlib.Tactic.CC.CCState.checkEqc (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Bool

Check for integrity of the CCState.

Equations

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

def Mathlib.Tactic.CC.CCState.checkInvariant (ccs : Mathlib.Tactic.CC.CCState) : Bool

Check for integrity of the CCState.

Equations

• ccs.checkInvariant = Batteries.RBMap.all ccs.entries fun (k : Lean.Expr) (n : Mathlib.Tactic.CC.Entry) => k != n.root || ccs.checkEqc k

def Mathlib.Tactic.CC.CCState.getNumROccs (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) (inLHS : Bool) : Nat

Equations

• ccs.getNumROccs e inLHS = match Batteries.RBMap.find? ccs.acEntries e with | some ent => Batteries.RBSet.size (ent.ROccs inLHS) | none => 0

def Mathlib.Tactic.CC.CCState.getVarWithLeastOccs (ccs : Mathlib.Tactic.CC.CCState) (e : Mathlib.Tactic.CC.ACApps) (inLHS : Bool) : Option Lean.Expr

Search for the AC-variable (Entry.acVar) with the least occurrences in the state.

Equations

• One or more equations did not get rendered due to their size.
• ccs.getVarWithLeastOccs (↑e₂_1) inLHS = some e₂_1

def Mathlib.Tactic.CC.CCState.getVarWithLeastLHSOccs (ccs : Mathlib.Tactic.CC.CCState) (e : Mathlib.Tactic.CC.ACApps) : Option Lean.Expr

Equations

• ccs.getVarWithLeastLHSOccs e = ccs.getVarWithLeastOccs e true

def Mathlib.Tactic.CC.CCState.getVarWithLeastRHSOccs (ccs : Mathlib.Tactic.CC.CCState) (e : Mathlib.Tactic.CC.ACApps) : Option Lean.Expr

Equations

• ccs.getVarWithLeastRHSOccs e = ccs.getVarWithLeastOccs e false

def Mathlib.Tactic.CC.CCState.ppEqc (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MessageData

Pretty print the entry associated with the given expression.

Equations

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

def Mathlib.Tactic.CC.CCState.ppEqcs (ccs : Mathlib.Tactic.CC.CCState) (nonSingleton : Bool := true) : Lean.MessageData

Pretty print the entire cc graph. If the nonSingleton argument is set to true then singleton equivalence classes will be omitted.

Equations

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

def Mathlib.Tactic.CC.CCState.ppParentOccsAux (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppParentOccs (ccs : Mathlib.Tactic.CC.CCState) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppACDecl (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppACDecls (ccs : Mathlib.Tactic.CC.CCState) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppACExpr (ccs : Mathlib.Tactic.CC.CCState) (e : Lean.Expr) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppACApps (ccs : Mathlib.Tactic.CC.CCState) : Mathlib.Tactic.CC.ACApps → Lean.MessageData

Equations

• One or more equations did not get rendered due to their size.
• ccs.ppACApps ↑e₂_1 = ccs.ppACExpr e₂_1

def Mathlib.Tactic.CC.CCState.ppACR (ccs : Mathlib.Tactic.CC.CCState) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppAC (ccs : Mathlib.Tactic.CC.CCState) : Lean.MessageData

Equations

• ccs.ppAC = (ccs.ppACDecls ++ Lean.MessageData.ofFormat (Std.Format.text "," ++ Lean.Format.line) ++ ccs.ppACR).sbracket

structure Mathlib.Tactic.CC.CCNormalizer : Type

The congruence closure module (optionally) uses a normalizer. The idea is to use it (if available) to normalize auxiliary expressions produced by internal propagation rules (e.g., subsingleton propagator).

• normalize : Lean.Expr → Lean.MetaM Lean.Expr

  The congruence closure module (optionally) uses a normalizer. The idea is to use it (if available) to normalize auxiliary expressions produced by internal propagation rules (e.g., subsingleton propagator).

structure Mathlib.Tactic.CC.CCPropagationHandler : Type

• propagated : Array Lean.Expr → Lean.MetaM Unit
• newAuxCCTerm : Lean.Expr → Lean.MetaM Unit

  Congruence closure module invokes the following method when a new auxiliary term is created during propagation.

structure Mathlib.Tactic.CC.CCStructureextends Mathlib.Tactic.CC.CCState : Type

CCStructure extends CCState (which records a set of facts derived by congruence closure) by recording which steps still need to be taken to solve the goal.

• ignoreInstances : Bool
• ac : Bool
• hoFns : Option (List Lean.Name)
• em : Bool
• values : Bool
• entries : Mathlib.Tactic.CC.Entries
• parents : Mathlib.Tactic.CC.Parents
• congruences : Mathlib.Tactic.CC.Congruences
• symmCongruences : Mathlib.Tactic.CC.SymmCongruences
• subsingletonReprs : Mathlib.Tactic.CC.SubsingletonReprs
• instImplicitReprs : Mathlib.Tactic.CC.InstImplicitReprs
• frozePartitions : Bool
• canOps : Mathlib.Tactic.CC.RBExprMap Lean.Expr
• opInfo : Mathlib.Tactic.CC.RBExprMap Bool
• acEntries : Mathlib.Tactic.CC.RBExprMap Mathlib.Tactic.CC.ACEntry
• acR : Mathlib.Tactic.CC.RBACAppsMap (Mathlib.Tactic.CC.ACApps × Mathlib.Tactic.CC.DelayedExpr)
• inconsistent : Bool
• gmt : Nat
• todo : Array Mathlib.Tactic.CC.TodoEntry

  Equalities that have been discovered but not processed.

• acTodo : Array Mathlib.Tactic.CC.ACTodoEntry

  AC-equalities that have been discovered but not processed.

• normalizer : Option Mathlib.Tactic.CC.CCNormalizer
• phandler : Option Mathlib.Tactic.CC.CCPropagationHandler
• cache : Mathlib.Tactic.CC.CCCongrTheoremCache

instance Mathlib.Tactic.CC.instInhabitedCCStructure : Inhabited Mathlib.Tactic.CC.CCStructure

Equations

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