16.12. 更大的例子🔗

16.12.1. 集成`grind`的功能🔗

该示例演示了grind的各个子模块如何无缝集成。特别是我们可以：

使用自定义模式实例化库中的定理，
执行案例分割，
进行线性整数算术推理，包括模块化条件，以及
进行 Gröbner 基础推理所有这些都没有提供明确的指令来驱动这些推理模式之间的相互作用。

对于此示例，我们将从实数的“模拟”版本以及 sin 和 cos 函数开始。当然，这个示例可以使用 Mathlib 的版本无需任何更改！

axiom R : Type


@[instance] axiom instCommRingR : Lean.Grind.CommRing R


axiom sin : R → R
axiom cos : R → R
axiom trig_identity : ∀ x, (cos x)^2 + (sin x)^2 = 1

我们的第一步是告诉grind在看到涉及sin或cos的目标时“将三角恒等式放在白板上”：

grind_pattern trig_identity => cos x
grind_pattern trig_identity => sin x

请注意，这里我们对同一定理使用“两种”不同模式，因此即使 grind 仅看到这些函数之一，该定理也会被实例化。如果我们希望仅当 sin 和 cos 都存在时更保守地实例化定理，我们可以使用多重模式：

grind_pattern trig_identity => cos x, sin x

对于本示例，两种方法都可以。

因为 grind 立即注意到三角恒等式，所以我们可以证明这样的目标：

example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := byx:R⊢ (cos x + sin x) ^ 2 = 2 * cos x * sin x + 1
  grindAll goals completed! 🐙

这里 grind 执行以下操作：

它注意到 cos x 和 sin x，因此实例化三角恒等式。
它注意到这是 CommRing R 中的多项式，并将其发送到 Gröbner 基础模块。此时不进行任何计算：它是该环中的第一个多项式关系，因此 Gröbner 基更新为 [(cos x)^2 + (sin x)^2 - 1]。
它注意到球门的左侧和右侧是 CommRing R 中的多项式，并将它们发送到 Gröbner 基础模块进行归一化。

由于它们模 (cos x)^2 + (sin x)^2 = 1 的范式相等，因此它们的等价类被合并，并且目标得到解决。

当需要同余闭包时，我们也可以进行此类论证：

example (f : R → Nat) :
    f ((cos x + sin x)^2) = f (2 * cos x * sin x + 1) := byx:Rf:R → Nat⊢ f ((cos x + sin x) ^ 2) = f (2 * cos x * sin x + 1)
  grindAll goals completed! 🐙

与之前一样，grind 实例化三角恒等式，注意到 (cos x + sin x)^2 和 2 * cos x * sin x + 1 等于模 (cos x)^2 + (sin x)^2 = 1，将这些代数表达式放在同一个等价类中，然后将函数应用程序 f ((cos x + sin x)^2) 和 f (2 * cos x * sin x + 1) 放在同一个等价类中，并关闭目标。

请注意，我们在这里使用了任意函数 f : R → Nat；让我们检查一下 grind 在 Gröbner 基步骤之后是否可以使用一些线性整数算术推理：

example (f : R → Nat) :
    4 * f ((cos x + sin x)^2) ≠ 2 + f (2 * cos x * sin x + 1) := byx:Rf✝:R → Natn:Natf:R → Nat⊢ 4 * f ((cos x + sin x) ^ 2) ≠ 2 + f (2 * cos x * sin x + 1)
  grindAll goals completed! 🐙

这里，grind 首先计算出对于某些 n : Nat，这个目标简化为 4 * n ≠ 2 + n（即通过如上所述识别两个函数应用），然后使用模块化来导出矛盾。

最后，我们还可以在某些情况下混合拆分：

example (f : R → Nat) :
    max 3 (4 * f ((cos x + sin x)^2)) ≠
      2 + f (2 * cos x * sin x + 1) := byx:Rf✝:R → Natn:Natf:R → Nat⊢ max 3 (4 * f ((cos x + sin x) ^ 2)) ≠ 2 + f (2 * cos x * sin x + 1)
  grindAll goals completed! 🐙

和以前一样，grind 首先进行识别两个函数应用程序所需的实例化和 Gröbner 基础计算。但是，cutsat 算法本身无法对 max 3 (4 * n) ≠ 2 + n 执行任何操作。接下来，在实例化声明 ∀ {n m : Nat}, max n m = if n ≤ m then m else n 的 Nat.max_def（自动，因为标准库中的注释）之后，grind 可以根据不等式进行大小写拆分。在分支3 ≤ 4 * n中，cutsat再次使用模块化来证明4 * n ≠ 2 + n。在分支4 * n < 3中，cutsat快速确定n = 0，然后注意到4 * 0 ≠ 2 + 0。

当然，这是一个非常人为的例子！在实践中，这种不同推理模式的自动集成非常强大：跟踪实例化定理和等价类的中央“白板”可以将相关术语和等式交给适当的模块（此处为 cutsat 和 Gröbner 库），然后模块可以将新事实返回到白板。

16.12.2. `if`-`then`-`else` 归一化🔗

此示例展示了 grind 的“开箱即用”功能。后面的示例将探索添加 @[grind] 注释作为开发过程的一部分，以使 grind 在新领域中更加有效。此示例不依赖于 grind 的任何代数扩展，我们只是使用：

从库中实例化带注释的定理，
同余闭包，以及
案件分割。

这里的解决方案建立在 Chris Hughes 早期的形式化基础上，但有一些显着的改进：

验证与代码分开，
现在证明是 fun_induction 和 grind 的单行组合，
该证明对于代码的更改（例如，将 HashMap 替换为 TreeMap）以及精确验证条件的更改具有鲁棒性。

16.12.2.1. 问题🔗

以下是 Rustan Leino 对问题的原始描述，如 Leonardo de Moura 发布在 Lean Zulip 上的描述：

数据结构是一个带有布尔文字、变量和 if-then-else 表达式的表达式。

目标是将此类表达式规范化为以下形式： a) 没有嵌套的 if：if 表达式的条件部分本身不是 if 表达式 b) 无常量测试：if 表达式的条件部分不是常量 c) 没有多余的 if：if 的 then 和 else 分支不同 d) 每个变量最多计算一次：条件的自由变量与 then 分支中的自由变量不相交，也与 else 分支中的自由变量不相交。

人们应该证明标准化函数产生满足这四个条件的表达式，并且还应该证明标准化函数保留了给定表达式的含义。

16.12.2.2. 正式声明🔗

为了形式化 Lean 中的语句，我们使用归纳类型IfExpr：

/--
An if-expression is either boolean literal, a
numbered variable, or an if-then-else expression
where each subexpression is an if-expression.
-/
inductive IfExpr
  | lit : Bool → IfExpr
  | var : Nat → IfExpr
  | ite : IfExpr → IfExpr → IfExpr → IfExpr
deriving DecidableEq

并定义一些归纳谓词和 eval 函数，因此我们可以声明四个所需的属性：

namespace IfExpr

/--
An if-expression has a "nested if" if it contains
an if-then-else where the "if" is itself an if-then-else.
-/
def hasNestedIf : IfExpr → Bool
  | lit _ => false
  | var _ => false
  | ite (ite _ _ _) _ _ => true
  | ite _ t e => t.hasNestedIf || e.hasNestedIf

/--
An if-expression has a "constant if" if it contains
an if-then-else where the "if" is itself a literal.
-/
def hasConstantIf : IfExpr → Bool
  | lit _ => false
  | var _ => false
  | ite (lit _) _ _ => true
  | ite i t e =>
    i.hasConstantIf || t.hasConstantIf || e.hasConstantIf

/--
An if-expression has a "redundant if" if
it contains an if-then-else where
the "then" and "else" clauses are identical.
-/
def hasRedundantIf : IfExpr → Bool
  | lit _ => false
  | var _ => false
  | ite i t e => t == e || i.hasRedundantIf ||
      t.hasRedundantIf || e.hasRedundantIf

/--
All the variables appearing in an if-expressions,
read left to right, without removing duplicates.
-/
def vars : IfExpr → List Nat
  | lit _ => []
  | var i => [i]
  | ite i t e => i.vars ++ t.vars ++ e.vars

/--
A helper function to specify that two lists are disjoint.
-/
def _root_.List.disjoint {α} [DecidableEq α] :
    List α → List α → Bool
  | [], _ => true
  | x::xs, ys => x ∉ ys && xs.disjoint ys

/--
An if expression evaluates each variable at most once if
for each if-then-else the variables in the "if" clause
are disjoint from the variables in the "then" clause
and the variables in the "if" clause
are disjoint from the variables in the "else" clause.
-/
def disjoint : IfExpr → Bool
  | lit _ => true
  | var _ => true
  | ite i t e =>
      i.vars.disjoint t.vars && i.vars.disjoint e.vars &&
        i.disjoint && t.disjoint && e.disjoint

/--
An if expression is "normalized" if it has
no nested, constant, or redundant ifs,
and it evaluates each variable at most once.
-/
def normalized (e : IfExpr) : Bool :=
  !e.hasNestedIf && !e.hasConstantIf &&
    !e.hasRedundantIf && e.disjoint

/--
The evaluation of an if expression
at some assignment of variables.
-/
def eval (f : Nat → Bool) : IfExpr → Bool
  | lit b => b
  | var i => f i
  | ite i t e => bif i.eval f then t.eval f else e.eval f

end IfExpr

使用这些我们可以陈述问题。面临的挑战是适应以下类型（并且做得很好！）：

def IfNormalization : Type :=
  { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }

16.12.2.3. 其他解决方案🔗

此时，值得暂停并至少执行以下操作之一：

尝试自己证明这一点！对于初学者来说是相当有挑战性的！你可以试试在 Live Lean 编辑器中，无需任何安装。
阅读 Chris Hughes 的解决方案，它包含在 Mathlib 存档中。该解决方案很好地利用了 Aesop，但并不理想，因为
1. 它使用子类型定义解决方案，同时给出其构造并证明其属性。我们认为在风格上最好将它们分开。
2. 即使使用 Aesop 自动化，在我们将其交给 Aesop 之前，仍然需要大约 15 行手动打样工作。
阅读 Wojciech Nawrocki 的解决方案。这一过程使用的自动化程度较低，校样工作量约为 300 行。

16.12.2.4. 使用`grind`的解决方案🔗

其实解决这个问题并不难：我们只需要一个递归函数来携带“已分配的变量”的记录，然后，每当对变量执行分支时，在每个分支中添加新的赋值。它还需要展平嵌套的 if-then-else 表达式，这些表达式在“条件”位置有另一个 if-then-else。（这是从 Chris Hughes 的解决方案中提取的，但没有子类型。）

让我们在 IfExpr 命名空间内工作。

namespace IfExpr

def fail to show termination for
  IfExpr.normalize
with errors
failed to infer structural recursion:
Cannot use parameter assign:
  the type HashMap Nat Bool does not have a `.brecOn` recursor
Cannot use parameter #2:
  failed to eliminate recursive application
    normalize assign (a.ite (b.ite t e) (c.ite t e))


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             #1 x2
1) 236:27-45  =  <
2) 237:27-45  =  <
3) 239:4-52   =  ?
4) 243:16-50  ?  _
5) 244:16-51  _  _
6) 246:16-50  _  _

#1: assign

Please use `termination_by` to specify a decreasing measure.normalize (assign : Std.HashMap Nat Bool) :
    IfExpr → IfExpr
  | lit b => lit b
  | var v =>
    match assign[v]? with
    | none => var v
    | some b => lit b
  | ite (lit true)  t _ => normalize assign t
  | ite (lit false) _ e => normalize assign e
  | ite (ite a b c) t e =>
    normalize assign (ite a (ite b t e) (ite c t e))
  | ite (var v)     t e =>
    match assign[v]? with
    | none =>
      let t' := normalize (assign.insert v true) t
      let e' := normalize (assign.insert v false) e
      if t' = e' then t' else ite (var v) t' e'
    | some b => normalize assign (ite (lit b) t e)

这非常简单，但它立即遇到了一个问题：

fail to show termination for
  IfExpr.normalize
with errors
failed to infer structural recursion:
Cannot use parameter assign:
  the type HashMap Nat Bool does not have a `.brecOn` recursor
Cannot use parameter #2:
  failed to eliminate recursive application
    normalize assign (a.ite (b.ite t e) (c.ite t e))


Could not find a decreasing measure.

Lean 这里告诉我们它看不到该函数正在终止。通常，Lean 非常擅长自行解决此问题，但对于足够复杂的函数我们需要介入并给予提示。

在这种情况下我们可以看到这是递归调用 ite (ite a b c) t e 正在 (ite a (ite b t e) (ite c t e)) 上调用 normalize Lean 遇到困难。 Lean 已对合理的终止措施进行了猜测，基于使用自动生成的 sizeOf 函数，但无法证明最终的目标，本质上是因为 t 和 e 在递归调用中多次出现。

为了解决这样的问题，我们几乎总是想停止使用自动生成的 sizeOf 函数，并构建我们自己的终止措施。我们将使用

@[simp] def normSize : IfExpr → Nat
  | lit _ => 0
  | var _ => 1
  | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1

许多不同的功能都可以在这里工作。基本思想是增加“condition”分支的“权重” （这是 2 * normSize i 中的乘法因子），因此，只要“condition”部分收缩一点，即使“then”和“else”分支增长，整个表达式也会被视为收缩。我们用 @[simp] 注释了该定义，因此允许 Lean 的自动终止检查器展开该定义。

完成此操作后，将使用 Lean.Parser.Command.declaration : commandtermination_by 子句进行定义：

def normalize (assign : Std.HashMap Nat Bool) :
    IfExpr → IfExpr
  | lit b => lit b
  | var v =>
    match assign[v]? with
    | none => var v
    | some b => lit b
  | ite (lit true)  t _ => normalize assign t
  | ite (lit false) _ e => normalize assign e
  | ite (ite a b c) t e =>
    normalize assign (ite a (ite b t e) (ite c t e))
  | ite (var v)     t e =>
    match assign[v]? with
    | none =>
      let t' := normalize (assign.insert v true) t
      let e' := normalize (assign.insert v false) e
      if t' = e' then t' else ite (var v) t' e'
    | some b => normalize assign (ite (lit b) t e)
termination_by e => e.normSize

现在是时候证明这个函数的一些属性了。我们只需将我们想要的所有属性打包在一起：

theorem declaration uses `sorry`normalize_spec
    (assign : Std.HashMap Nat Bool) (e : IfExpr) :
    (normalize assign e).normalized
      ∧ (∀ f, (normalize assign e).eval f =
          e.eval fun w => assign[w]?.getD (f w))
      ∧ ∀ (v : Nat),
          v ∈ vars (normalize assign e) → ¬ v ∈ assign :=
  sorry

即：

normalize 的结果实际上是根据初始定义进行归一化的，
如果我们使用一些赋值规范化“if-then-else”表达式，然后评估剩余的变量，我们得到与使用两个赋值的组合评估原始“if-then-else”相同的结果，
并且赋值中出现的任何变量都不再出现在规范化表达式中。

您可能认为我们应该将这三个属性表述为单独的引理，但事实证明一次证明它们真的很方便，因为我们可以使用 fun_induction 策略假设所有这些属性在递归调用中适用于 normalize，然后 grind 会将所有事实放在一起得出结果：

-- We tell `grind` to unfold our definitions above.
attribute [local grind]
  normalized hasNestedIf hasConstantIf hasRedundantIf
  disjoint vars eval List.disjoint

theorem normalize_spec
    (assign : Std.HashMap Nat Bool) (e : IfExpr) :
    (normalize assign e).normalized
      ∧ (∀ f, (normalize assign e).eval f =
          e.eval fun w => assign[w]?.getD (f w))
      ∧ ∀ (v : Nat),
          v ∈ vars (normalize assign e) → ¬ v ∈ assign := byassign:HashMap Nat Boole:IfExpr⊢ (normalize assign e).normalized = true ∧
  (∀ (f : Nat → Bool), eval f (normalize assign e) = eval (fun w => assign[w]?.getD (f w)) e) ∧
    ∀ (v : Nat), v ∈ (normalize assign e).vars → ¬v ∈ assign
  fun_induction normalize with grindAll goals completed! 🐙

fun_induction 和 grind 组合在这里工作的事实有点令人惊讶。我们对此感到非常兴奋，我们希望看到更多这种风格的证明！

高度自动化证明的一个可爱的结果是，您通常可以灵活地更改语句，根本不改变证明！作为例子，我们上面断言的特定方式 “赋值中出现的任何变量不再出现在规范化表达式中” 可以用许多不同的方式来表述（尽管没有省略！）。变化其实并不重要，和 grind 都可以证明和使用其中的任何一个：

这里我们使用assign.contains v = false：

example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
    (normalize assign e).normalized
      ∧ (∀ f, (normalize assign e).eval f =
          e.eval fun w => assign[w]?.getD (f w))
      ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) →
          assign.contains v = false := byassign:HashMap Nat Boole:IfExpr⊢ (normalize assign e).normalized = true ∧
  (∀ (f : Nat → Bool), eval f (normalize assign e) = eval (fun w => assign[w]?.getD (f w)) e) ∧
    ∀ (v : Nat), v ∈ (normalize assign e).vars → assign.contains v = false
  fun_induction normalize with grindAll goals completed! 🐙

这里我们使用 assign[v]? = none：

example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
    (normalize assign e).normalized
      ∧ (∀ f, (normalize assign e).eval f =
          e.eval fun w => assign[w]?.getD (f w))
      ∧ ∀ (v : Nat),
          v ∈ vars (normalize assign e) → assign[v]? = none := byassign:HashMap Nat Boole:IfExpr⊢ (normalize assign e).normalized = true ∧
  (∀ (f : Nat → Bool), eval f (normalize assign e) = eval (fun w => assign[w]?.getD (f w)) e) ∧
    ∀ (v : Nat), v ∈ (normalize assign e).vars → assign[v]? = none
  fun_induction normalize with grindAll goals completed! 🐙

事实上，我们是否使用 grind 也没有什么影响 HashMap 或 TreeMap 用于存储分配，我们可以简单地切换该实现细节，而无需触及证明：

def normalize (assign : Std.TreeMap Nat Bool) :
    IfExpr → IfExpr
  | lit b => lit b
  | var v =>
    match assign[v]? with
    | none => var v
    | some b => lit b
  | ite (lit true)  t _ => normalize assign t
  | ite (lit false) _ e => normalize assign e
  | ite (ite a b c) t e =>
    normalize assign (ite a (ite b t e) (ite c t e))
  | ite (var v)     t e =>
    match assign[v]? with
    | none =>
      let t' := normalize (assign.insert v true) t
      let e' := normalize (assign.insert v false) e
      if t' = e' then t' else ite (var v) t' e'
    | some b => normalize assign (ite (lit b) t e)
termination_by e => e.normSize

theorem normalize_spec
    (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
    (normalize assign e).normalized
      ∧ (∀ f, (normalize assign e).eval f =
          e.eval fun w => assign[w]?.getD (f w))
      ∧ ∀ (v : Nat),
          v ∈ vars (normalize assign e) → ¬ v ∈ assign := byassign:TreeMap Nat Bool comparee:IfExpr⊢ (normalize assign e).normalized = true ∧
  (∀ (f : Nat → Bool), eval f (normalize assign e) = eval (fun w => assign[w]?.getD (f w)) e) ∧
    ∀ (v : Nat), v ∈ (normalize assign e).vars → ¬v ∈ assign
  fun_induction normalize with grindAll goals completed! 🐙

（我们能够做到这一点的事实依赖于这样一个事实：grind 所需的 HashMap 和 TreeMap 的所有引理都已在标准库中进行了注释。）

如果您想尝试一下这段代码，您可以在此处找到整个文件，或者事实上无需安装即可使用在实时 Lean 编辑器中。