16.3. 同余闭包🔗

同余闭包在“等于”的自反、对称和传递闭包下维护术语的等价类并且相等的参数产生相等的函数结果的规则。形式上，如果 a = a' 和 b = b'，则添加 f a b = f a' b'。该算法合并等价类，直到达到固定点。如果发现矛盾，那么可以立即关闭目标。

用共享白板来比喻：

每个假设 h : t₁ = t₂ 都写一条连接 t₁ 和 t₂ 的线。
每当两项通过一条或多条线连接时，它们就被认为是相等的。很快，整个星座（f a、g (f a)，...）就连接起来了。
如果同一归纳类型的两个不同构造函数通过一根或多根线连接，则发现矛盾并关闭目标。例如，将 True 和 False 或 none 和 some 1 等同起来会产生矛盾。

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! 🐙

最初，f y、g y、x 和 y 位于不同的等价类中。同余闭包引擎使用 h₁ 合并 x 和 y，之后等价类为 {x, y}, f y 和 g y。接下来，h₂ 用于合并 f y 和 g y，之后的类为 {x, y} and {f y, g y}。这足以证明f x = g x，因为y和x属于同一类。

类似的推理也适用于构造函数：

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! 🐙

由于对构造函数 Prod.mk 遵循同余，因此只要将 a 和 b 放置在同一类中，元组就变得相等。

Live ↪

16.3.1. 同余闭包与简化🔗

同余闭包是与简化完全不同的操作：

simp 重写目标，一旦看到 h : t₁ = t₂，就将出现的 t₁ 替换为 t₂。重写是定向的、破坏性的。
grind 双向累加相等。没有术语被重写；相反，两位代表住在同一个班级。所有其他引擎（E 匹配、理论求解器、传播）都可以查询这些类并添加新事实，然后闭包增量更新。

这使得同余闭包在存在对称推理、相互递归和构造函数的大型嵌套（重写会重复工作）的情况下特别强大。