mathlib documentation

core.init.meta.smt.congruence_closure

structure cc_config :

Type

ignore_instances : bool
ac : bool
ho_fns : option (list name)
em : bool

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.

meta constant cc_state.mk_core (a : cc_config) :

meta constant cc_state.mk_using_hs_core (a : cc_config) :

tactic cc_state

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

meta constant cc_state.next (a : cc_state) (a_1 : 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.

meta constant cc_state.roots_core (a : cc_state) (a_1 : bool) :

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 (a : cc_state) (a_1 : expr) :

Get the root representative of the given expression.

meta constant cc_state.mt (a : cc_state) (a_1 : expr) :

"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 (a : cc_state) :

"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 (a : cc_state) :

Increment the Global Modification time.

meta constant cc_state.is_cg_root (a : cc_state) (a_1 : expr) :

Check if e is the root of the congruence class.

meta constant cc_state.pp_eqc (a : cc_state) (a_1 : expr) :

Pretty print the entry associated with the given expression.

meta constant cc_state.pp_core (a : cc_state) (a_1 : bool) :

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 (a : cc_state) (a_1 : expr) :

tactic cc_state

Add the given expression to the graph.

meta constant cc_state.add (a : cc_state) (a_1 : expr) :

tactic cc_state

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 (a : cc_state) (a_1 a_2 : expr) :

Check whether two expressions are in the same equivalence class.

meta constant cc_state.is_not_eqv (a : cc_state) (a_1 a_2 : expr) :

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

meta constant cc_state.eqv_proof (a : cc_state) (a_1 a_2 : expr) :

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

meta constant cc_state.inconsistent (a : cc_state) :

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 (a : cc_state) (a_1 : expr) :

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

meta constant cc_state.refutation_for (a : cc_state) (a_1 : expr) :

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

meta constant cc_state.proof_for_false (a : cc_state) :

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

meta def cc_state.mk :

meta def cc_state.mk_using_hs :

tactic cc_state

meta def cc_state.roots (s : cc_state) :

@[instance]

meta def cc_state.has_to_tactic_format :

has_to_tactic_format cc_state

meta def cc_state.eqc_of_core (s : cc_state) (a a_1 : expr) (a_2 : list expr) :

meta def cc_state.eqc_of (s : cc_state) (e : expr) :

meta def cc_state.in_singlenton_eqc (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 a : expr) (a_1 : α) :

α

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 tactic.cc :

meta def tactic.cc_dbg_core (cfg : cc_config) :

meta def tactic.cc_dbg :

meta def tactic.ac_refl :