在Hoare一章中所介绍的霍尔逻辑可以被认为是“模型论”的：每一个构造子 的证明规则以关于求值行为的'定理'的形式呈现，并且程序正确性（霍尔三元组的有 效性）的证明由在Coq里面直接组合这些定理所构造。 另外一种介绍霍尔逻辑的方式是定义一个完全分开的证明系统——关于命令，霍尔三元组 等等的一系列公理和推断规则——接着说明霍尔三元组的一个证明是在'那个'逻辑中的一 个合法导出式。这可以通过给出在这个新逻辑中的'合法导出式'的归纳定义来实现。 这一章是可选的。在阅读之前，你会想要阅读一下在'逻辑基础'（'软件基础'的 第一卷）中的 ProofObjects 章节。

定义

我们并不需要包含对应 hoare_consequence_pre 或 hoare_consequence_post 的公理， 因为它们可以简单地通过 H_Consequence 被证明。

作为一个例子，让我们构造一个证明对象，来表示这个霍尔三元组的一个导出式
      {{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}
      X::=X+1 ;; X::=X+2
      {{X=3}}.

我们可以让 Coq 的策略来帮助我们构造这个证明对象。

性质

练习：2 星, standard (hoare_proof_sound)

请证明由 hoare_proof 构造的推导式对应于有效的霍尔三元组。换言之，就是 hoare_proof 推导式是'可靠'的。提示：我们已经将Hoare 中所有独立的证明规则证明成了定理 hoare_skip、hoare_asgn 等等。 请发挥它们的优势。

我们也可以使用Coq的推理工具来证明关于霍尔逻辑的元定理。例如，下述是我们在 Hoare 章节中看到的两条定理的模拟——这一次，使用霍尔逻辑导出式（可证明 性），而不是直接使用霍尔三元组的语义，来表达这些定理。 第一条定理表达，对于所有的 P 和 c，断言 {{P}} c {{True}} 在霍尔逻辑中是 '可证明的'。注意到这个证明比在Hoare中的语义证明更加复杂：实际上我们需要在命令 c 的结构上应用归纳法 。

类似地，我们可以说明对于任意的 c 和 Q，{{False}} c {{Q}} 是可证明的。

最后，我们可以说明 hoare_proof 公理集合足够用来证明关于任何（部分）正确性的 事实。更准确地说，任何我们能够证明的语义霍尔三元组，都能够通过这些公理证明。 这样的公理集合被称为'相对完备的（relatively complete）'。也就是说，这些公理 '相对于'我们可以用底层的断言语言证明的事实来说是完备的。 如果该语言的证明中有所跳跃（gap），那么我们应该责怪它而非霍尔逻辑公理。 我们的证明的灵感来自于： https://www.ps.uni-saarland.de/courses/sem-ws₁₁/script/Hoare.html 为了完成这个证明，我们需要使用一种被称为'最弱前置条件（Weakest Precondition）' 的技术装置来创造一些中间的断言（它也在 Hoare2 有所讨论）。 给定一个命令c和一个想要的后置条件断言 Q ，最弱前置条件 wp c Q 是一个断言 P，使得 {{P}} c {{Q}} 成立，并且对于任意其他断言 P'，如果 {{P}} c {{Q}} 成立，那么 P' → P。我们可以更加直接地将其定义为：

为了习惯这个 wp 的定义，请证明以下两个简单的定理。

练习：1 星, standard (wp_is_precondition)

练习：1 星, standard (wp_is_weakest)

练习：2 星, standard (wp_invariant)

Prove that for any Q, assertion wp (WHILE b DO c END) Q is an invariant of WHILE b DO c END.

以下辅助引理在接下来的练习中会很有用。

练习：4 星, standard (hoare_proof_complete)

完成如下定理的证明。对 WHILE 分支的提示：你需要创建一个循环不变量。

最后，我们可能希望我们的公理霍尔逻辑是'可决定的（decidable）'；也就是说，这里 有一个（会终止的）算法（一个'决定性过程（decision procedure）'）来决定一个给 定的霍尔三元组是否是合法的（可导出的）。但是这样的一个决定性过程并不存在！ 考虑三元组 {{True}} c {{False}}。这个三元组是有效的当且仅当 c 不终止。这意味着， 任何一个能够决定任意三元组的合法性的算法能够解决停机问题（Halting Problem）。 类似地，三元组 {{True}} SKIP {{P}} 是合法的当且仅当 ∀ s, P s 是合法的，其中 P 是Coq逻辑的任意一个断言。但是我们已知对于这个逻辑并没有任何的决定性过程。 总而言之，此公理化表述更清晰地诠释如何“出具霍尔逻辑下的证明”。 但是，从实际上我们需要写出这些证明的角度来看，这并不让人完全 满意：这太冗长了。在 Hoare2 一章中的关于形式化修饰程序的章节会向我们展 示如何做的更好。