16.4. 约束传播🔗

约束传播作用于白板上的 True 与 False 两个桶。每当某个项被加入其中一个桶时，grind 都会触发许多小型的 前向规则，从它的逻辑后果中推导出更多信息：

布尔联结词

布尔联结词的真值表可用于推出更多为真或为假的事实。例如：

如果 A 是 True，那么 A ∨ B 就变成 True。
如果 A ∧ B 是 True，那么 A 和 B 都会变成 True。
如果 A ∧ B 是 False，那么 A、B 中至少有一个会变成 False。

归纳类型

如果由同一个归纳类型的两个不同构造子应用而成的项（例如 none 和 some）被放进同一个等价类，就会导出矛盾。如果由同一个构造子应用而成的两个项被放进同一个等价类，那么它们的参数也会被判定为相等。

投影

从 h : (x, y) = (x', y') 可以推出 x = x' 和 y = y'。

强制转换

任意项 cast h a : β 都会立刻与 a : α 判定为相等（使用异质相等）。

归约

定义性归约也会传播，因此 (a, b).1 会与 a 判定为相等。

下面给出一组具有代表性的传播器片段，用来展示它们的整体风格。它们都遵循同一套骨架。

检查子表达式的真值。
如果还能推出更多事实，就要么用 (pushEq) 将项判定为相等（也就是把它们连接到比喻意义上的白板上），要么用 (pushEqTrue / pushEqFalse) 标示真值。这些步骤会借助诸如 Grind.and_eq_of_eq_true_left 这样的内部辅助引理来构造证明项。
如果出现矛盾，就用 (closeGoal) 关闭目标。

向上传播从子项的事实中推出关于整个项的事实，而 向下传播则从整个项的事实中推出关于子项的事实。

/-- 对合取进行*向上*的相等传播。 -/
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)

/--
当整个 `And` 已被证明为 `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

其他经常触发的传播器也遵循同样的模式：

传播器	处理对象	说明
`propagateOrUp` / `propagateOrDown`	`A ∨ B`	使用析取的真值表来推出更多真值
`propagateNotUp` / `propagateNotDown`	`¬ A`	确保 `¬ A` 与 `A` 的真值相反
`propagateEqUp` / `propagateEqDown`	`a = b`	桥接布尔值，检测构造子冲突
`propagateIte` / `propagateDIte`	`ite` / `dite`	一旦已知条件的真值，就把该项与选中的分支判定为相等
`propagateEtaStruct`	带有 `[grind ext]` 标记的结构体值	生成 η‑展开 `a = ⟨a.1, …⟩`

许多针对 Bool 的专门变体都严格仿照这些规则（例如 propagateBoolAndUp）。

16.4.1. 仅靠传播的示例🔗

下面这些目标纯粹依靠约束传播即可关闭——既不需要分类讨论，也不需要理论求解器：

-- 布尔联结词：a && !a 永远为 false。
example (a : Bool) : (a && !a) = false := bya:Bool⊢ (a && !a) = false
  grindAll goals completed! 🐙

-- 条件表达式（ite）：
-- 一旦条件为真，ite 就会选择 then 分支。
example (c : Bool) (t e : Nat) (h : c = true) :
    (if c then t else e) = t := byc:Boolt:Nate:Nath:c = true⊢ (if c = true then t else e) = t
  grindAll goals completed! 🐙

-- 否定会向下传播真值。
example (a : Bool) (h : (!a) = true) : a = false := bya:Boolh:(!a) = true⊢ a = false
  grindAll goals completed! 🐙

这些片段会立刻运行完成，因为相关传播器（propagateBoolAndUp、propagateIte、propagateBoolNotDown）会在假设被内化后立刻触发。将选项 trace.grind.eqc 设为 true 后，每当两个等价类合并时，grind 都会打印一行信息，这很适合观察传播是如何发生的。

传播规则的集合会随着时间不断扩展和细化，因此 InfoView 中显示的 True 与 False 桶也会越来越丰富。完整的等价类只会在 grind 失败时自动显示，而且只针对它无法关闭的第一个子目标——可以利用这些输出来检查缺失的事实，并理解为什么该子目标仍然未解。

识别缺失的事实

在这个例子中，grind 失败了：

example :
    x = y ∧ y = z →
    w = x ∨ w = v →
    w = z := byα✝:Sort u_1x:α✝y:α✝z:α✝w:α✝v:α✝⊢ x = y ∧ y = z → w = x ∨ w = v → w = z
  `grind` failed
grindα:Sort u_1x y z w v:αleft:x = yright:y = zh_1:w = x ∨ w = vh_2:¬w = z⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x = y
[prop] y = z
[prop] w = x ∨ w = v
[prop] ¬w = z
[eqc] True propositions
[prop] w = x ∨ w = v
[prop] w = v
[eqc] False propositions
[prop] w = x
[prop] w = z
[eqc] Equivalence classes
[eqc] {x, y, z}
[eqc] {w, v}grindAll goals completed! 🐙

生成的错误消息会给出识别到的等价类，以及为真和为假的命题：

`grind` failed
grindα:Sort u_1x y z w v:αleft:x = yright:y = zh_1:w = x ∨ w = vh_2:¬w = z⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x = y
[prop] y = z
[prop] w = x ∨ w = v
[prop] ¬w = z
[eqc] True propositions
[prop] w = x ∨ w = v
[prop] w = v
[eqc] False propositions
[prop] w = x
[prop] w = z
[eqc] Equivalence classes
[eqc] {x, y, z}
[eqc] {w, v}

x = y 和 y = z 都是由约束传播从前提 x = y ∧ y = z 中发现的。在这个证明中，grind 对 w = x ∨ w = v 做了分类讨论。在第二个分支里，它无法把 w 和 z 放进同一个等价类。