时间戳

首页 > 解决方案 > 一对空的“证明 qed”在 Isabelle 中是如何工作的？

isabelle - 一对空的“证明 qed”在 Isabelle 中是如何工作的？

问题描述

在 Isabelle 2020 文档 classes.pdf pp.10 中，有一个看起来很奇怪的证明序列：（proof qed auto为了说明目的分为三行），这真的让我感到困惑：

interpretation list_monoid: monoid append "[]"
proof
qed
auto

所以证明似乎是空的（在proof和之间qed），然后是一个auto。如果将鼠标放在证明位置，则显示三个目标：

goal (3 subgoals):
 1. ⋀x y z. (x @ y) @ z = x @ y @ z
 2. ⋀x. [] @ x = x
 3. ⋀x. x @ [] = x

在 处qed，目标消失。然后，auto似乎什么都不做。

有人可以帮助解释proof qed ...结构是如何工作的吗？

就 Izar 与应用样式模式而言，在每一行proof, qed和auto行中，系统处于哪种模式？

标签： isabelle

解决方案

范式的解释qed m可以在官方文档（Isar-ref）的 6.4.2 小节中找到：

proof:证明（证明）-> 证明（状态）

qed:证明(状态) -> 证明(状态) | 本地理论 | 理论

  1. 初始细化步骤proof m1将新陈述的目标减少为稍后要解决的许多子目标。m1如果由证明（链）模式指示，则将事实传递给 前向链接。
  1. 最终结论步骤qed m2旨在解决剩余的目标。没有事实传递给m2.

如果继续阅读，还有更详细的解释：

proof m1用证明方法细化目标m1；如果证明（链）模式指示，则通过前向链接的事实。

qed m2通过证明方法细化任何剩余的目标，m2并通过假设得出子证明。如果目标是show，则某些未决子目标也将通过导出到封闭目标上下文的结果产生的规则来解决。因此qed可能会因两个原因而失败：要么m2失败，要么结果规则不适合封闭上下文的任何未决目标。

qed因此，在尝试解决剩下的目标时传递一个方法是完全合法的。在上面的示例中，有效地，在应用调用的默认细化步骤后剩余的所有目标proof都由 解决auto。

by m1 m2通常可以用来代替proof m1 qed m2（唯一的区别是by m1 m2回溯m1和m2）。因此，我相信证明原始问题中的定理的另一种常规方法是

interpretation list_monoid: monoid append "[]"
  by unfold_locales auto

有关描述，by另请参见 Isar-ref 中的第 6.4.2 小节。

证明定理的一种稍微不那么传统的方法，但更接近proof qed auto原始问题中的范式是

interpretation list_monoid: monoid append "[]"
  apply standard 
  apply auto
  done

最后，当然，您不需要使用qed m范式解决所有目标。下面的代码清单展示了该范例的最标准用例：

interpretation list_monoid: monoid append "[]"
proof
  show 
    "(x @ y) @ z = x @ y @ z" 
    "[] @ x = x"
    for x y z :: "'a list"
    by auto
qed auto

答案是基于 Isabelle2021-RC2 编写的。

推荐阅读