16.4. 约束传播
约束传播 适用于白板的 True 和 False 存储桶。
每当将术语添加到其中一个存储桶时，grind 都会触发数十个小型 forward 规则，这些规则从其逻辑结果中获取更多信息：
- 布尔连接词
- 归纳类型
如果将同一 归纳类型 的两个不同构造函数（例如
none和some）的应用所形成的项置于同一等价类中，则会产生矛盾。 如果由同一构造函数的应用形成的两个项被放置在同一等价类中，则它们的参数也相等。- 预测
从
h : (x, y) = (x', y')中我们得出x = x'和y = y'。- 演员阵容
- 减少
定义归约被传播，因此
(a, b).1等同于a。
下面是传播者的代表性切片，展示了它们的整体风格。 每个都遵循相同的骨架。
-
它检查子表达式的真值。
-
如果可以导出进一步的事实，它可以使用 (
pushEq) 使术语相等（在隐喻白板上连接它们），或者使用 (pushEqTrue/pushEqFalse) 指示真值。 这些步骤使用内部辅助引理（例如Grind.and_eq_of_eq_true_left）生成证明项。 -
如果出现矛盾，则使用 (
closeGoal) 关闭目标。
向上传播从有关子项的事实导出有关项的事实，而向下传播从有关项的事实导出有关子项的事实。
/-- Propagate equalities *upwards* for conjunctions. -/
builtin_grind_propagator propagateAndUp ↑And := fun e => do
let_expr And a b := e | return ()
if (← isEqTrue a) then
-- a = True ⇒ (a ∧ b) = b
pushEq e b <|
mkApp3 (mkConst ``Grind.and_eq_of_eq_true_left)
a b (← mkEqTrueProof a)
else if (← isEqTrue b) then
-- b = True ⇒ (a ∧ b) = a
pushEq e a <|
mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right)
a b (← mkEqTrueProof b)
else if (← isEqFalse a) then
-- a = False ⇒ (a ∧ b) = False
pushEqFalse e <|
mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left)
a b (← mkEqFalseProof a)
else if (← isEqFalse b) then
-- b = False ⇒ (a ∧ b) = False
pushEqFalse e <|
mkApp3 (mkConst ``Grind.and_eq_of_eq_false_right)
a b (← mkEqFalseProof b)
/--
Truth flows *down* when the whole `And` is proven `True`.
-/
builtin_grind_propagator propagateAndDown ↓And :=
fun e => do
if (← isEqTrue e) then
let_expr And a b := e | return ()
let h ← mkEqTrueProof e
-- (a ∧ b) = True ⇒ a = True
pushEqTrue a <| mkApp3
(mkConst ``Grind.eq_true_of_and_eq_true_left) a b h
-- (a ∧ b) = True ⇒ B = True
pushEqTrue b <| mkApp3
(mkConst ``Grind.eq_true_of_and_eq_true_right) a b h
其他频繁触发的传播器遵循相同的模式：
传播者 | 手柄 | 注释 |
|---|---|---|
|
| 使用真值表进行析取以导出进一步的真值 |
|
|
确保 |
|
| 桥接布尔值，检测构造函数冲突 |
|
| 一旦条件的真值已知，则将该项与所选分支等同 |
|
标记为 |
生成 η 展开式 |
Bool 的许多专门变体完全反映了这些规则（例如 propagateBoolAndUp）。
16.4.1. 仅传播示例
这些目标“纯粹”通过约束传播来封闭——没有案例分割，没有理论求解器：
-- Boolean connective: a && !a is always false.
example (a : Bool) : (a && !a) = false := a:Bool⊢ (a && !a) = false
All goals completed! 🐙
-- Conditional (ite):
-- once the condition is true, ite picks the 'then' branch.
example (c : Bool) (t e : Nat) (h : c = true) :
(if c then t else e) = t := c:Boolt:Nate:Nath:c = true⊢ (if c = true then t else e) = t
All goals completed! 🐙
-- Negation propagates truth downwards.
example (a : Bool) (h : (!a) = true) : a = false := a:Boolh:(!a) = true⊢ a = false
All goals completed! 🐙
这些片段会立即运行，因为一旦假设被内化，相关传播器（propagateBoolAndUp、propagateIte、propagateBoolNotDown）就会立即触发。
将选项 trace.grind.eqc 设置为 true 会导致 grind 每次两个等价类合并时打印一行，这对于查看实际传播非常方便。
传播规则集随着时间的推移而扩展和完善，因此 InfoView 将显示越来越丰富的 True 和 False 存储桶。
完整的等价类仅在 grind 失败时自动显示，并且仅针对无法关闭的第一个子目标 - 使用此输出来检查缺失的事实并了解子目标保持打开状态的原因。