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

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.

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

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

Ordering on Expr.

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

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

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.

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.

instance Mathlib.Tactic.CC.instBEqCCCongrTheoremKey : BEq CCCongrTheoremKey

instance Mathlib.Tactic.CC.instHashableCCCongrTheoremKey : Hashable CCCongrTheoremKey

@[reducible, inline]

abbrev Mathlib.Tactic.CC.CCCongrTheoremCache : Type

Caches used to find corresponding CCCongrTheorems.

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 CCConfig

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

instance Mathlib.Tactic.CC.instBEqACApps : BEq ACApps

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

def Mathlib.Tactic.CC.instOrdACApps : Ord ACApps

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

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.

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₁

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

Appends arguments of e to r.

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.

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

Sorts args and applies them to ACApps.apps.

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

Flattens given two ACApps.

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.

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

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

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.

instance Mathlib.Tactic.CC.instInhabitedDelayedExpr : Inhabited DelayedExpr

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

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

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

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

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.

instance Mathlib.Tactic.CC.instInhabitedEntry : Inhabited Entry

@[reducible, inline]

abbrev Mathlib.Tactic.CC.Entries : Type

Stores equivalence class data associated with an expression e.

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

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

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

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.

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

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.

instance Mathlib.Tactic.CC.instBEqCongruencesKey : BEq CongruencesKey

instance Mathlib.Tactic.CC.instHashableCongruencesKey : Hashable CongruencesKey

@[reducible, inline]

abbrev Mathlib.Tactic.CC.Congruences : Type

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

structure Mathlib.Tactic.CC.SymmCongruencesKey : Type

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

instance Mathlib.Tactic.CC.instBEqSymmCongruencesKey : BEq SymmCongruencesKey

instance Mathlib.Tactic.CC.instHashableSymmCongruencesKey : Hashable SymmCongruencesKey

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

@[reducible, inline]

abbrev Mathlib.Tactic.CC.SubsingletonReprs : Type

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

@[reducible, inline]

abbrev Mathlib.Tactic.CC.InstImplicitReprs : Type

Stores the root representatives of .instImplicit arguments.

@[reducible, inline]

abbrev Mathlib.Tactic.CC.TodoEntry : Type

@[reducible, inline]

abbrev Mathlib.Tactic.CC.ACTodoEntry : Type

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.

instance Mathlib.Tactic.CC.instInhabitedCCState : Inhabited CCState

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.

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

Get the root representative of the given expression.

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.

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

Check if e is the root of the congruence class.

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.

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

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.

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

Check for integrity of the CCState.

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

Check for integrity of the CCState.

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

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.

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.

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.

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

Pretty print the entry associated with the given expression.

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.

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

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

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

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

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

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

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

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

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