# Congruence closure #

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by
cc


As an example requiring some thinking to do by hand, consider:

example (f : ℕ → ℕ) (x : ℕ)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x := by
cc


The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.

The cc implementation in Lean does a few more tricks: for example it derives a = b from Nat.succ a = Nat.succ b, and Nat.succ a != Nat.zero for any a.

Make an new CCState from the given config.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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.

Equations
• ccs.rootsCore nonsingleton = (ccs.getRoots #[] nonsingleton).toList
Instances For

Increment the Global Modification time.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Add the given expression to the graph.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Add the given proof term as a new rule. The proof term H must be an Eq _ _, HEq _ _, Iff _ _, or a negation of these.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Check whether two expressions are in the same equivalence class.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

proofFor cc e constructs a proof for e if it is equivalent to true in CCState

Equations
• One or more equations did not get rendered due to their size.
Instances For

refutationFor cc e constructs a proof for Not e if it is equivalent to False in CCState

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
Instances For

The root expressions for each equivalence class in the graph.

Equations
• s.roots = s.rootsCore true
Instances For
Equations

Continue to append following expressions in the equivalence class of e to r until f is found.

The equivalence class of e.

Equations
• s.eqcOf e = s.eqcOfCore e e []
Instances For

The size of the equivalence class of e.

Equations
• s.eqcSize e = (s.eqcOf e).length
Instances For
partial def Mathlib.Tactic.CC.CCState.foldEqcCore {α : Sort u_1} (f : α) (first : Lean.Expr) (c : Lean.Expr) (a : α) :
α

Fold f over the equivalence class of c, accumulating the result in a. Loops until the element first is encountered.

See foldEqc for folding f over all elements of the equivalence class.

def Mathlib.Tactic.CC.CCState.foldEqc {α : Sort u_1} (e : Lean.Expr) (a : α) (f : α) :
α

Fold the function of f over the equivalence class of e.

Equations
• s.foldEqc e a f = s.foldEqcCore f e e a
Instances For
def Mathlib.Tactic.CC.CCState.foldEqcM {α : Type} {m : } [] (e : Lean.Expr) (a : α) (f : αLean.Exprm α) :
m α

Fold the monadic function of f over the equivalence class of e.

Equations
• s.foldEqcM e a f = s.foldEqc e (pure a) fun (act : m α) (e : Lean.Expr) => do let aact f a e
Instances For
def Lean.MVarId.cc (m : Lean.MVarId) (cfg : optParam Mathlib.Tactic.CC.CCConfig { ignoreInstances := true, ac := true, hoFns := none, em := true, values := false }) :

Applies congruence closure to solve the given metavariable. This procedure tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b).

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas. The cc implementation in Lean does a few more tricks: for example it derives a = b from Nat.succ a = Nat.succ b, and Nat.succ a != Nat.zero for any a.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Allow elaboration of CCConfig arguments to tactics.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ℕ) (f : ℕ → ℕ) (h: a = b) (h' : b = c) : f a = f c := by
cc


As an example requiring some thinking to do by hand, consider:

example (f : ℕ → ℕ) (x : ℕ)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x := by
cc

Equations
• One or more equations did not get rendered due to their size.
Instances For