mathlib3 documentation

core / init.meta.smt.congruence_closure

source
structure cc_config  :
Type
Instances for cc_config
source
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
source
meta constant cc_state.mk_core  :
cc_config → cc_state
source
meta constant cc_state.mk_using_hs_core  :
cc_config → tactic cc_state

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

source
meta constant cc_state.next  :
cc_state → expr → 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.

source
meta constant cc_state.roots_core  :
cc_state → bool → list expr

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.

source
meta constant cc_state.root  :
cc_state → expr → expr

Get the root representative of the given expression.

source
meta constant cc_state.mt  :
cc_state → 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.

source
meta constant cc_state.gmt  :
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.

source
meta constant cc_state.inc_gmt  :
cc_state → cc_state

Increment the Global Modification time.

source
meta constant cc_state.is_cg_root  :
cc_state → expr → bool

Check if e is the root of the congruence class.

source
meta constant cc_state.pp_eqc  :
cc_state → expr → tactic format

Pretty print the entry associated with the given expression.

source
meta constant cc_state.pp_core  :
cc_state → bool → tactic format

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

source
meta constant cc_state.internalize  :
cc_state → expr → tactic cc_state

Add the given expression to the graph.

source
meta constant cc_state.add  :
cc_state → 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.

source
meta constant cc_state.is_eqv  :
cc_state → expr → expr → tactic bool

Check whether two expressions are in the same equivalence class.

source
meta constant cc_state.is_not_eqv  :
cc_state → expr → expr → tactic bool

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

source
meta constant cc_state.eqv_proof  :
cc_state → expr → expr → tactic expr

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

source
meta constant cc_state.inconsistent  :
cc_state → bool

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

source
meta constant cc_state.proof_for  :
cc_state → expr → tactic expr

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

source
meta constant cc_state.refutation_for  :
cc_state → expr → tactic expr

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

source
meta constant cc_state.proof_for_false  :
cc_state → tactic expr

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

source
meta def cc_state.mk  :
cc_state
source
meta def cc_state.mk_using_hs  :
tactic cc_state
source
meta def cc_state.roots (s : cc_state) :
list expr
source
@[protected, instance]
meta def cc_state.has_to_tactic_format  :
has_to_tactic_format cc_state
source
meta def cc_state.eqc_of_core (s : cc_state) :
expr → expr → list expr → list expr
source
meta def cc_state.eqc_of (s : cc_state) (e : expr) :
list expr
source
meta def cc_state.in_singlenton_eqc (s : cc_state) (e : expr) :
bool
source
meta def cc_state.eqc_size (s : cc_state) (e : expr) :
ℕ
source
meta def cc_state.fold_eqc_core {α : Sort u_1} (s : cc_state) (f : α → expr → α) (first : expr) :
expr → α → α
source
meta def cc_state.fold_eqc {α : Sort u_1} (s : cc_state) (e : expr) (a : α) (f : α → expr → α) :
α
source
meta def cc_state.mfold_eqc {α : Type} {m : Type → Type} [monad m] (s : cc_state) (e : expr) (a : α) (f : α → expr → m α) :
m α
source
meta def tactic.cc_core (cfg : cc_config) :
tactic unit
source
meta def tactic.cc  :
tactic unit
source
meta def tactic.cc_dbg_core (cfg : cc_config) :
tactic unit
source
meta def tactic.cc_dbg  :
tactic unit
source
meta def tactic.ac_refl  :
tactic unit