mathlib3 documentation

core / init.meta.smt.congruence_closure

structure cc_config  :
Instances for cc_config
meta constant cc_state  :

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 cc_state and congruence, that is, if a = b then f(a) = f(b) and so on.

Instances for cc_state

Create a congruence closure state object using the hypotheses in the current goal.

meta constant  :

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.

Returns the root expression for each equivalence class in the graph. If the bool argument is set to true then it only returns roots of non-singleton classes.

meta constant cc_state.root  :

Get the root representative of the given expression.

meta constant  :

"Modification Time". The field m_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 m_mt records the last time any proper descendant of of thie entry was involved in a merge.

meta constant cc_state.gmt  :

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

Increment the Global Modification time.

Check if e is the root of the congruence class.

Pretty print the entry associated with the given expression.

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

Add the given expression to the graph.

Add the given proof term as a new rule. The proof term p must be an eq _ _, heq _ _, iff _ _, or a negation of these.

Check whether two expressions are in the same equivalence class.

Check whether two expressions are not in the same equivalence class.

Returns a proof term that the given terms are equivalent in the given cc_state

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

proof_for cc e constructs a proof for e if it is equivalent to true in cc_state

refutation_for cc e constructs a proof for not e if it is equivalent to false in cc_state

If the given state is inconsistent, return a proof for false. Otherwise fail.

meta def  :
meta def cc_state.roots (s : cc_state) :
meta def cc_state.eqc_of (s : cc_state) (e : expr) :
meta def cc_state.eqc_size (s : cc_state) (e : expr) :
meta def cc_state.fold_eqc_core {α : Sort u_1} (s : cc_state) (f : α expr α) (first : expr) :
expr α α
meta def cc_state.fold_eqc {α : Sort u_1} (s : cc_state) (e : expr) (a : α) (f : α expr α) :
meta def cc_state.mfold_eqc {α : Type} {m : Type Type} [monad m] (s : cc_state) (e : expr) (a : α) (f : α expr m α) :
m α
meta def tactic.cc_core (cfg : cc_config) :
meta def  :