The Lean Language Reference

17.4. Congruence Closure

17.4.1. What is congruence closure?

Congruence closure maintains equivalence classes of terms under the reflexive–symmetric–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 classes until a fixed point is reached.

Think of a shared white‑board:

  1. Every hypothesis h : t₁ = t₂ writes a line connecting t₁ and t₂.

  2. Each merge paints both terms the same color. Soon whole constellations (f a, g (f a), …) share the color.

  3. If True and False ever land in the same color—or likewise two different constructors of the same inductive type such as none and some 1—the goal is closed by contradiction.

17.4.2. How it differs from simp

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

17.4.3. Minimal examples

example {α} (f g : α → α) (x y : α) (h₁ : x = y) (h₂ : f y = g y) : f x = g x := α:Sort u_1f:α → αg:α → αx:αy:αh₁:x = yh₂:f y = g y⊢ f x = g x -- After h₁, x and y share a class, -- h₂ adds f y = g y, and -- closure bridges to f x = g x All goals completed! 🐙 example (a b c : Nat) (h : a = b) : (a, c) = (b, c) := a:Natb:Natc:Nath:a = b⊢ (a, c) = (b, c) -- Pair constructor obeys congruence, -- so once a = b the tuples are equal All goals completed! 🐙