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

source
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)

Instances For

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

Instances For

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

Instances For

source
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 }

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.ExprMap (α : Type u) :
Type u

Red-black maps whose keys are `Expr`s.

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

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.ExprSet :
Type

Red-black sets of `Expr`s.

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

Instances For

source
structure Mathlib.Tactic.CC.CCCongrTheorem extends Lean.Meta.CongrTheorem :
Type

`CongrTheorem`s 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`.

Instances For

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

Instances For

source
structure Mathlib.Tactic.CC.CCCongrTheoremKey :
Type

Keys used to find corresponding `CCCongrTheorem`s.

- fn : Lean.Expr

  The function of the given `CCCongrTheorem`.

- nargs : ℕ

  The number of arguments of `fn`.

Instances For

source
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

Instances For

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

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

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

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

source
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)

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.CCCongrTheoremCache :
Type

Caches used to find corresponding `CCCongrTheorem`s.

Equations

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

Instances For

source
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

Instances For

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

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

Instances For

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

- Mathlib.Tactic.CC.instInhabitedCCConfig = { default := Mathlib.Tactic.CC.instInhabitedCCConfig.default }

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

Instances For

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

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

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

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

Instances For

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

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

source
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

Instances For

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

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

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
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₁))

Instances For

source
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

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.ACAppsMap (α : Type u) :
Type u

Red-black maps whose keys are `ACApps`es.

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

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.ACAppsSet :
Type

Red-black sets of `ACApps`es.

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

Instances For

source
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`.

Instances For

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

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

Instances For

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

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

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

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

source
inductive Mathlib.Tactic.CC.EntryExpr :
Type

This is used as a proof term in `Entry`s 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`.

Instances For

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

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

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

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

Instances For

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

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

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

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

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

Instances For

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

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

Instances For

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

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

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

Instances For

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

Instances For

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

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

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

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

Instances For

source
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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.ParentOccSet :
Type

Red-black sets of `ParentOcc`s.

Equations

- Mathlib.Tactic.CC.ParentOccSet = Std.TreeSet Mathlib.Tactic.CC.ParentOcc (Ordering.byKey Mathlib.Tactic.CC.ParentOcc.expr compare)

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

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

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

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

source
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)

Instances For

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

Instances For

source
structure Mathlib.Tactic.CC.SymmCongruencesKey :
Type

- h₁ : Lean.Expr
- h₂ : Lean.Expr

Instances For

source
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

Instances For

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

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

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

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

source
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)

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.CC.TodoEntry :
Type
Equations

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

Instances For

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

Instances For

source
structure Mathlib.Tactic.CC.CCState extends 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`.

Instances For

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

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

Instances For

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

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

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

source
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).

Instances For

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

Instances For

source
structure Mathlib.Tactic.CC.CCStructure extends 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

Instances For

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

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

source
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 }

Instances For