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.ExprMap (α : Type u) : Type u

Red-black maps whose keys are Exprs.

TODO: the choice between TreeMap and HashMap is not obvious: 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.ExprMap α = Std.TreeMap Lean.Expr α compare

@[reducible, inline]

abbrev Mathlib.Tactic.CC.ExprSet : Type

Red-black sets of Exprs.

TODO: the choice between TreeSet and HashSet is not obvious: 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.ExprSet = Std.TreeSet Lean.Expr compare

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

CongrTheorems equipped with additional infos used by congruence closure modules.

• type : Expr
• proof : Expr
• argKinds : Array 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 : ℕ) : Lean.MetaM (Option 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 : ℕ

  The number of arguments of fn.

def Mathlib.Tactic.CC.instBEqCCCongrTheoremKey.beq : CCCongrTheoremKey → CCCongrTheoremKey → Bool

Equations

• Mathlib.Tactic.CC.instBEqCCCongrTheoremKey.beq { fn := a, nargs := a_1 } { fn := b, nargs := b_1 } = (a == b && a_1 == b_1)
• Mathlib.Tactic.CC.instBEqCCCongrTheoremKey.beq x✝¹ x✝ = false

instance Mathlib.Tactic.CC.instBEqCCCongrTheoremKey : BEq CCCongrTheoremKey

Equations

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

instance Mathlib.Tactic.CC.instHashableCCCongrTheoremKey : Hashable CCCongrTheoremKey

Equations

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

def Mathlib.Tactic.CC.instHashableCCCongrTheoremKey.hash : CCCongrTheoremKey → UInt64

Equations

• Mathlib.Tactic.CC.instHashableCCCongrTheoremKey.hash { fn := a, nargs := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[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

def Mathlib.Tactic.CC.instInhabitedCCConfig.default : CCConfig

Equations

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

instance Mathlib.Tactic.CC.instInhabitedCCConfig : Inhabited CCConfig

Equations

• Mathlib.Tactic.CC.instInhabitedCCConfig = { default := Mathlib.Tactic.CC.instInhabitedCCConfig.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) : ACApps

  An ACApps of just an Expr.

• apps (op : Lean.Expr) (args : Array Lean.Expr) : 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 ACApps

Equations

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

def Mathlib.Tactic.CC.instInhabitedACApps.default : ACApps

Equations

• Mathlib.Tactic.CC.instInhabitedACApps.default = ↑default

instance Mathlib.Tactic.CC.instBEqACApps : BEq ACApps

Equations

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

def Mathlib.Tactic.CC.instBEqACApps.beq : ACApps → ACApps → Bool

Equations

• Mathlib.Tactic.CC.instBEqACApps.beq ↑a ↑b = (a == b)
• Mathlib.Tactic.CC.instBEqACApps.beq (Mathlib.Tactic.CC.ACApps.apps a a_1) (Mathlib.Tactic.CC.ACApps.apps b b_1) = (a == b && a_1 == b_1)
• Mathlib.Tactic.CC.instBEqACApps.beq x✝¹ x✝ = false

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

Equations

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

def Mathlib.Tactic.CC.instOrdACApps : Ord 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₂ : 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₂ : 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 : 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₂ : 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) : 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₂ : ACApps) : 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 : 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.ACAppsMap (α : Type u) : Type u

Red-black maps whose keys are ACAppses.

TODO: the choice between TreeMap and HashMap is not obvious: 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.ACAppsMap α = Std.TreeMap Mathlib.Tactic.CC.ACApps α compare

@[reducible, inline]

abbrev Mathlib.Tactic.CC.ACAppsSet : Type

Red-black sets of ACAppses.

TODO: the choice between TreeSet and HashSet is not obvious: 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.ACAppsSet = Std.TreeSet 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) : DelayedExpr

  A DelayedExpr of just an Expr.

• eqProof (lhs rhs : Lean.Expr) : 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 : DelayedExpr) : DelayedExpr

  Will be applied to congr_arg.

• congrFun (h : DelayedExpr) (a : ACApps) : DelayedExpr

  Will be applied to congr_fun.

• eqSymm (h : DelayedExpr) : DelayedExpr

  Will be applied to Eq.symm.

• eqSymmOpt (a₁ a₂ : ACApps) (h : DelayedExpr) : DelayedExpr

  Will be applied to Eq.symm.

• eqTrans (h₁ h₂ : DelayedExpr) : DelayedExpr

  Will be applied to Eq.trans.

• eqTransOpt (a₁ a₂ a₃ : ACApps) (h₁ h₂ : DelayedExpr) : DelayedExpr

  Will be applied to Eq.trans.

• heqOfEq (h : DelayedExpr) : DelayedExpr

  Will be applied to heq_of_eq.

• heqSymm (h : DelayedExpr) : DelayedExpr

  Will be applied to HEq.symm.

def Mathlib.Tactic.CC.instInhabitedDelayedExpr.default : DelayedExpr

Equations

• Mathlib.Tactic.CC.instInhabitedDelayedExpr.default = ↑default

instance Mathlib.Tactic.CC.instInhabitedDelayedExpr : Inhabited DelayedExpr

Equations

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

instance Mathlib.Tactic.CC.instCoeExprDelayedExpr : Coe Lean.Expr 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) : EntryExpr

  An EntryExpr of just an Expr.

• congr : EntryExpr

  dummy congruence proof, it is just a placeholder.

• eqTrue : EntryExpr

  dummy eq_true proof, it is just a placeholder

• refl : EntryExpr

  dummy refl proof, it is just a placeholder.

• ofDExpr (e : DelayedExpr) : EntryExpr

  An EntryExpr of a DelayedExpr.

instance Mathlib.Tactic.CC.instInhabitedEntryExpr : Inhabited EntryExpr

Equations

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

def Mathlib.Tactic.CC.instInhabitedEntryExpr.default : EntryExpr

Equations

• Mathlib.Tactic.CC.instInhabitedEntryExpr.default = ↑default

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

Equations

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

instance Mathlib.Tactic.CC.instCoeExprEntryExpr : Coe Lean.Expr 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 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 : ℕ

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

• mt : ℕ

  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.

def Mathlib.Tactic.CC.instInhabitedEntry.default : Entry

Equations

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

instance Mathlib.Tactic.CC.instInhabitedEntry : Inhabited Entry

Equations

• Mathlib.Tactic.CC.instInhabitedEntry = { default := Mathlib.Tactic.CC.instInhabitedEntry.default }

@[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.ExprMap 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 : ℕ

  Natural number associated to an expression.

• RLHSOccs : ACAppsSet

  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 : ACAppsSet

  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 ACEntry

Equations

• Mathlib.Tactic.CC.instInhabitedACEntry = { default := Mathlib.Tactic.CC.instInhabitedACEntry.default }

def Mathlib.Tactic.CC.instInhabitedACEntry.default : ACEntry

Equations

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

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

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 = Std.TreeSet 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.ExprMap Mathlib.Tactic.CC.ParentOccSet

inductive Mathlib.Tactic.CC.CongruencesKey : Type

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

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

• ho (fn arg : Lean.Expr) : CongruencesKey

  fn is Higher-Order.

def Mathlib.Tactic.CC.instBEqCongruencesKey.beq : CongruencesKey → CongruencesKey → Bool

Equations

• Mathlib.Tactic.CC.instBEqCongruencesKey.beq (Mathlib.Tactic.CC.CongruencesKey.fo a a_1) (Mathlib.Tactic.CC.CongruencesKey.fo b b_1) = (a == b && a_1 == b_1)
• Mathlib.Tactic.CC.instBEqCongruencesKey.beq (Mathlib.Tactic.CC.CongruencesKey.ho a a_1) (Mathlib.Tactic.CC.CongruencesKey.ho b b_1) = (a == b && a_1 == b_1)
• Mathlib.Tactic.CC.instBEqCongruencesKey.beq x✝¹ x✝ = false

instance Mathlib.Tactic.CC.instBEqCongruencesKey : BEq CongruencesKey

Equations

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

instance Mathlib.Tactic.CC.instHashableCongruencesKey : Hashable CongruencesKey

Equations

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

def Mathlib.Tactic.CC.instHashableCongruencesKey.hash : CongruencesKey → UInt64

Equations

• Mathlib.Tactic.CC.instHashableCongruencesKey.hash (Mathlib.Tactic.CC.CongruencesKey.fo a a_1) = mixHash (mixHash 0 (hash a)) (hash a_1)
• Mathlib.Tactic.CC.instHashableCongruencesKey.hash (Mathlib.Tactic.CC.CongruencesKey.ho a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)

@[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

def Mathlib.Tactic.CC.instBEqSymmCongruencesKey.beq : SymmCongruencesKey → SymmCongruencesKey → Bool

Equations

• Mathlib.Tactic.CC.instBEqSymmCongruencesKey.beq { h₁ := a, h₂ := a_1 } { h₁ := b, h₂ := b_1 } = (a == b && a_1 == b_1)
• Mathlib.Tactic.CC.instBEqSymmCongruencesKey.beq x✝¹ x✝ = false

instance Mathlib.Tactic.CC.instBEqSymmCongruencesKey : BEq SymmCongruencesKey

Equations

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

instance Mathlib.Tactic.CC.instHashableSymmCongruencesKey : Hashable SymmCongruencesKey

Equations

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

def Mathlib.Tactic.CC.instHashableSymmCongruencesKey.hash : SymmCongruencesKey → UInt64

Equations

• Mathlib.Tactic.CC.instHashableSymmCongruencesKey.hash { h₁ := a, h₂ := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[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, this uses FastSingleton instead of Subsingleton.

Equations

• Mathlib.Tactic.CC.SubsingletonReprs = Mathlib.Tactic.CC.ExprMap 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.ExprMap (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 : Entries

  Maps known expressions to their equivalence class data.

• parents : Parents

  Maps an expression e to the expressions e occurs in.

• congruences : Congruences

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

• symmCongruences : SymmCongruences

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

• subsingletonReprs : SubsingletonReprs

  Stores the root representatives of subsingletons, this uses FastSingleton instead of Subsingleton.

• instImplicitReprs : 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 : ExprMap Lean.Expr

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

• opInfo : ExprMap Bool

  Whether the canonical operator is supported by AC.

• acEntries : ExprMap ACEntry

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

• acR : ACAppsMap (ACApps × 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 : ℕ

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

def Mathlib.Tactic.CC.instInhabitedCCState.default : CCState

Equations

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

instance Mathlib.Tactic.CC.instInhabitedCCState : Inhabited CCState

Equations

• Mathlib.Tactic.CC.instInhabitedCCState = { default := Mathlib.Tactic.CC.instInhabitedCCState.default }

def Mathlib.Tactic.CC.CCState.mkEntryCore (ccs : CCState) (e : Lean.Expr) (interpreted constructor : Bool) : 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 : CCState) (e : Lean.Expr) : Lean.Expr

Get the root representative of the given expression.

Equations

• ccs.root e = match ccs.entries[e]? with | some n => n.root | none => e

def Mathlib.Tactic.CC.CCState.next (ccs : 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 ccs.entries[e]? with | some n => n.next | none => e

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

Check if e is the root of the congruence class.

Equations

• ccs.isCgRoot e = match ccs.entries[e]? with | some n => e == n.cgRoot | none => true

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

"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 ccs.entries[e]? with | some n => n.mt | none => ccs.gmt

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

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

Equations

• ccs.inSingletonEqc e = match ccs.entries[e]? with | some it => it.next == e | none => true

def Mathlib.Tactic.CC.CCState.getRoots (ccs : 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 : 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 : CCState) : Bool

Check for integrity of the CCState.

Equations

• ccs.checkInvariant = Std.TreeMap.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 : CCState) (e : Lean.Expr) (inLHS : Bool) : ℕ

Equations

• ccs.getNumROccs e inLHS = match ccs.acEntries[e]? with | some ent => Std.TreeSet.size (ent.ROccs inLHS) | none => 0

def Mathlib.Tactic.CC.CCState.getVarWithLeastOccs (ccs : CCState) (e : 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 : CCState) (e : ACApps) : Option Lean.Expr

Search for the AC-variable (Entry.acVar) with the fewest occurrences in the LHS.

Equations

• ccs.getVarWithLeastLHSOccs e = ccs.getVarWithLeastOccs e true

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

Search for the AC-variable (Entry.acVar) with the fewest occurrences in the RHS.

Equations

• ccs.getVarWithLeastRHSOccs e = ccs.getVarWithLeastOccs e false

def Mathlib.Tactic.CC.CCState.ppEqc (ccs : 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 : 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 : 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 : CCState) : Lean.MessageData

Equations

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

def Mathlib.Tactic.CC.CCState.ppACDecl (ccs : 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 : CCState) : Lean.MessageData

Equations

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

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

Equations

• ccs.ppACExpr e = match ccs.acEntries[e]? with | some it => (Lean.MessageData.ofFormat ∘ Std.format) (toString "x_" ++ toString it.idx) | x => Lean.MessageData.ofExpr e

def Mathlib.Tactic.CC.CCState.ppACApps (ccs : CCState) : 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 : CCState) : Lean.MessageData

Equations

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

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

Equations

• ccs.ppAC = (ccs.ppACDecls ++ Lean.MessageData.ofFormat (Std.Format.text "," ++ Std.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 : Entries
• parents : Parents
• congruences : Congruences
• symmCongruences : SymmCongruences
• subsingletonReprs : SubsingletonReprs
• instImplicitReprs : InstImplicitReprs
• frozePartitions : Bool
• canOps : ExprMap Lean.Expr
• opInfo : ExprMap Bool
• acEntries : ExprMap ACEntry
• acR : ACAppsMap (ACApps × DelayedExpr)
• inconsistent : Bool
• gmt : ℕ
• todo : Array TodoEntry

  Equalities that have been discovered but not processed.

• acTodo : Array ACTodoEntry

  AC-equalities that have been discovered but not processed.

• normalizer : Option CCNormalizer
• phandler : Option CCPropagationHandler
• cache : CCCongrTheoremCache

instance Mathlib.Tactic.CC.instInhabitedCCStructure : Inhabited CCStructure

Equations

• Mathlib.Tactic.CC.instInhabitedCCStructure = { default := Mathlib.Tactic.CC.instInhabitedCCStructure.default }

def Mathlib.Tactic.CC.instInhabitedCCStructure.default : CCStructure

Equations

• Mathlib.Tactic.CC.instInhabitedCCStructure.default = { toCCState := default, todo := default, acTodo := default, normalizer := default, phandler := default, cache := default }