操作系统形式化验证实践教程(11) - 结构化证明语言Isar

结构化证明语言Isar基本语法

apply方法和by方法虽然可以完成功能，但是看起来更像是命令式语言。使用Isar语言，还可以写得更加形式化一点。

Isar的格式看起来像这样:

proof
  assume "公式1"
  from “公式1" have "公式2" by 方法
  ...
  from "公式n" show "结论" by 方法
qed

虽然换了种写法，但是其实核心内容并没有变。

直接proof指定方法

最简单的写法，就是把by的内容放到proof语句之后，然后就直接qed了。
我们看7个例子：

lemma A1: "A ⟹ (B⟹A)"
proof(erule thin_rl,Pure.assumption)
qed

lemma A2 : "(A ⟹ (B⟹C))  ⟹ ((A⟹B) ⟹ (A⟹C))"
proof(erule meta_impE,assumption,assumption)
qed

lemma A3: "(A∧B) ⟹ A"
proof(erule conjunct1)
qed

lemma A4: "(A∧B) ⟹ B"
proof(erule conjunct2)
qed

lemma A5: "A ⟹ (B ⟹ (A∧B))"
proof(erule conjI,assumption)
qed

lemma A6: "A ⟹ (A ∨ B)"
proof(erule disjI1)
qed

lemma A7: "B ⟹ (A ∨ B)"
proof(erule disjI2)
qed

assume have show

下面我们尝试用assume...have...show的方法改写一下。proof语句的参数我们给个"-"，表示空值：

lemma "(A ⟹ (B⟹C))  ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -
  assume Fact0: "(A ⟹ (B⟹C))"
  from Fact0 show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed

this

上一节我们在assume和show中使用了标签，但是Isar认为使用标签是不好的，容易给词法分析造成困扰。
如果使用上一条中的公式，我们就直接使用this来指代，上一节的例子就变成这样：

lemma "(A ⟹ (B⟹C))  ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -
  assume "(A ⟹ (B⟹C))"
  from this show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed

then

尽可能使用this之后，我们发现from this用的很广泛，于是我们可以给from this起一个别名叫then。于是上节的例子可以写成下面这样：

lemma "(A ⟹ (B⟹C))  ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -
  assume "(A ⟹ (B⟹C))"
  then show "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed

thus和hence

换成then之后，我们发现from this终于被隐藏起来了。但是，大量的then have和then show又出来了。于是我们可以再简化一下，给then have起个别名hence，给then show起个别名thus。
于是上节的例子可以写成这样：

lemma "(A ⟹ (B⟹C))  ⟹ ((A⟹B) ⟹ (A⟹C))"
proof -
  assume "(A ⟹ (B⟹C))"
  thus "((A⟹B) ⟹ (A⟹C))" by (rule meta_impE)
qed

假设拆分

当lemma比较长时，可以将其拆分成几个独立的假设，然后在proof中使用。
我们来看个例子：

lemma impE_2:
  assumes 1:‹P⟶Q›
  and 2: ‹Q⟹R›
  and 3: ‹P⟶Q ⟹ P›
  shows ‹R›
proof -
  from 3 and 1 have ‹P› by simp
  with 1 have ‹Q› by (rule impE)
  with 2 show ‹R› by simp
qed

这里我们又使用了一个新的缩写with，with xxx等于from xxx this，是from的一个语法糖。
其中的"‹",写作<open>。同样“›”写作<close>. 也可以通过"来输入，然后IDE中会提示。

我们来看ASCII源码：

lemma impE_2:
  assumes 1:\<open>P\<longrightarrow>Q\<close>
  and 2: \<open>Q\<Longrightarrow>R\<close>
  and 3: \<open>P\<longrightarrow>Q \<Longrightarrow> P\<close>
  shows \<open>R\<close>
proof -
  from 3 and 1 have \<open>P\<close> by simp
  with 1 have \<open>Q\<close> by (rule impE)
  with 2 show \<open>R\<close> by simp
qed

对了，针对这样分立条件的，不使用Isar的情况下该如何写呢？我们可以使用using来使用假设们然后再用by来引用证明方法，来看个例子：

lemma impE_3:
  assumes 1:‹P⟶Q›
  and 2: ‹Q⟹R›
  and 3: ‹P⟶Q ⟹ P›
shows ‹R›
  using "1" "2" "3" by blast

巩固下，再来个例子：

lemma notE_2:
  assumes 1: ‹¬P›
and 2:‹¬P ⟹ P›
shows ‹R›
  using "1" "2" by auto

小结

Isar语言的出现，是希望能够能通过一些语法糖，让证明看起来更像是用自然语言书写，提升可读性。
但是其基本原理跟没有Isar语言框架是一致的。数理逻辑知识目前仍然是主要要攻克的点，而非语言和框架。