# 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`

.

The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)

The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

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

- Mathlib.Tactic.CC.CCState.mkUsingHs = Mathlib.Tactic.CC.CCState.mkUsingHsCore { ignoreInstances := true, ac := true, hoFns := none, em := true, values := false }

## Instances For

The root expressions for each equivalence class in the graph.

## Instances For

## Equations

- Mathlib.Tactic.CC.CCState.instToMessageData = { toMessageData := fun (s : Mathlib.Tactic.CC.CCState) => s.ppEqcs }

Continue to append following expressions in the equivalence class of `e`

to `r`

until `f`

is
found.

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.

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

Fold the monadic function of `f`

over the equivalence class of `e`

.

## Equations

## Instances For

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`

.

- The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)
- The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

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