mathlib documentation

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.

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

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.

Get the root representative of the given expression.

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

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

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.