mathlib documentation

core / init.meta.smt.congruence_closure

structure cc_config  :
Type
Instances for cc_config
meta constant cc_state  :
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 cc_state and congruence, that is, if a = b then f(a) = f(b) and so on.

Instances for cc_state
meta constant cc_state.mk_core  :

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

meta constant cc_state.next  :

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.

meta constant cc_state.roots_core  :

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 cc_state.mt  :
cc_stateexpr

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

meta constant cc_state.inc_gmt  :

Increment the Global Modification time.

meta constant cc_state.is_cg_root  :

Check if e is the root of the congruence class.

meta constant cc_state.pp_eqc  :

Pretty print the entry associated with the given expression.

meta constant cc_state.pp_core  :

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

meta constant cc_state.internalize  :

Add the given expression to the graph.

meta constant cc_state.add  :

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

meta constant cc_state.is_eqv  :

Check whether two expressions are in the same equivalence class.

meta constant cc_state.is_not_eqv  :

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

meta constant cc_state.eqv_proof  :

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

meta constant cc_state.inconsistent  :

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

meta constant cc_state.proof_for  :

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

meta constant cc_state.refutation_for  :

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 cc_state.mk  :
meta def cc_state.roots (s : cc_state) :
meta def cc_state.eqc_of_core (s : cc_state) :
exprexprlist exprlist expr
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 : α → exprm α) :
m α
meta def tactic.cc_core (cfg : cc_config) :
meta def tactic.cc  :