17.2. Congruence Closure🔗

Congruence closure maintains equivalence classes of terms under the reflexive, symmetric, and transitive closure of “is equal to” and the rule that equal arguments yield equal function results. Formally, if a = a' and b = b', then f a b = f a' b' is added. The algorithm merges equivalence classes until a fixed point is reached. If a contradiction is discovered, then the goal can be closed immediately.

Using the analogy of the shared whiteboard:

Every hypothesis h : t₁ = t₂ writes a line connecting t₁ and t₂.
Whenever two terms are connected by one or more lines, they're considered to be equal. Soon, whole constellations (f a, g (f a), …) are connected.
If two different constructors of the same inductive type are connected by one or more lines, then a contradiction is discovered and the goal is closed. For example, equating True and False or none and some 1 would be a contradiction.

Congruence Closure

This theorem is proved using congruence closure:

example {α} (f g : α → α) (x y : α)
    (h₁ : x = y) (h₂ : f y = g y) :
    f x = g x := byα:Sort u_1f:α → αg:α → αx:αy:αh₁:x = yh₂:f y = g y⊢ f x = g x
  grindAll goals completed! 🐙

Initially, f y, g y, x, and y are in separate equivalence classes. The congruence closure engine uses h₁ to merge x and y, after which the equivalence classes are {x, y}, f y, and g y. Next, h₂ is used to merge f y and g y, after which the classes are {x, y} and {f y, g y}. This is sufficient to prove that f x = g x, because y and x are in the same class.

Similar reasoning is used for constructors:

example (a b c : Nat) (h : a = b) : (a, c) = (b, c) := bya:Natb:Natc:Nath:a = b⊢ (a, c) = (b, c)
  grindAll goals completed! 🐙

Because the pair constructor Prod.mk obeys congruence, the tuples become equal as soon as a and b are placed in the same class.

17.2.1. Congruence Closure vs. Simplification

Congruence closure is a fundamentally different operation from simplification:

simp rewrites a goal, replacing occurrences of t₁ with t₂ as soon as it sees h : t₁ = t₂. The rewrite is directional and destructive.
grind accumulates equalities bidirectionally. No term is rewritten; instead, both representatives live in the same class. All other engines ( E‑matching, theory solvers, propagation) can query these classes and add new facts, then the closure updates incrementally.

This makes congruence closure especially robust in the presence of symmetrical reasoning, mutual recursion, and large nestings of constructors where rewriting would duplicate work.