操作系统形式化验证实践教程(12) - 经典命题逻辑与公式查错方法

第10节我们介绍了直觉一阶逻辑，它是不接受排中律的逻辑。在编程体感上，直觉一阶逻辑IFOL库，不支持auto，不支持sledgehammer，不能使用try0与try，基本上可以使用的就是simp或者手动推理。

经典命题逻辑我们使用经典一阶逻辑库FOL，它是继承自IFOL的。

经典一阶逻辑库FOL

现在我们换成经典一阶逻辑的FOL库，现在可以使用auto了，我们看个例子：

theory fol2
  imports FOL
begin
lemma D3: "⟦(¬A ⟹ B);(¬A ⟹¬B)⟧⟹ A"
proof (auto)
qed
end

我们来个复杂点的例子：

lemma E1 : 
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬B ⟶ A›

从一堆公式中取出一个，可以采用local访问的方式，根据下标的不同来进行获取，比如取第n个可以用local.assms(n)，也可以直接local.n，我们看例子：

lemma E2_1: 
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬A ⟶ B›
  by (rule local.assms(1))

lemma E2_2:
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬A›
  by (rule local.assms(3))

lemma E2_3:
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬B›
  by (rule local.assms(2))

于是，按照《面向计算机科学的数理逻辑》中的写法，我们的公式推导可以写成下面这样：

lemma E1 : 
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬B ⟶ A›
proof -
  from "1" "2" "3" have 1: ‹¬A ⟶ B› by (rule E2_1)
  from "1" "2" "3" have 3: ‹¬A› by (rule E2_2)
  from "1" "2" "3" have 2: ‹¬B› by (rule E2_3)
  from "1" "3" have 4: ‹B› by (rule mp)
  from "1" "2" "4" have 5: ‹A› by simp
  from "1" "5" show ‹¬B ⟶ A› by simp
qed

其中，from 1 3 have 4的过程是个小三段论：

proof (prove)
using this:
    ¬ A ⟶ B
    ¬ A

goal (1 subgoal):
 1. B

from 1 2 4 have 5，我们单独写个定理试试，有notE, notE', contrapos_np等规则可以用：

lemma Test1: "⟦(¬A ⟶ B);B;¬B⟧⟹A"
  by (rule contrapos_np)

上节我们学习了，如果使用上一条的结论this，可以使用with来简化书写，我们把顺序调整一下：

lemma E2 : 
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬B ⟶ A›
proof -
  from "1" "2" "3" have 1: ‹¬A ⟶ B› by (rule E2_1)
  from "1" "2" "3" have 2: ‹¬B› by (rule E2_3)
  from "1" "2" "3" have 3: ‹¬A› by (rule E2_2)
  with "1" have 4: ‹B› by (rule mp)
  with "1" "2" have 5: ‹A› by simp
  with "1" show ‹¬B ⟶ A› by simp
qed

因为我们的assumes其实可以直接使用，我们可以简化一下：

lemma E2_v2 : 
  assumes 1: ‹¬A ⟶ B›
and 2: ‹¬B›
and 3: ‹¬A›
shows ‹¬B ⟶ A›
proof -
  from "1" "3" have 4: ‹B› by (rule mp)
  with "1" "2" have 5: ‹A› by simp
  with "1" show ‹¬B ⟶ A› by simp
qed

常用经典命题逻辑定理

蕴含相关定理

lemma H1_1 : "(A⟶B) ⟹ (A⟹B)"
  by(rule mp)

lemma H1_2: "A ⟹ (B⟶A)"
  by simp

lemma H1_3: "⟦A⟶B; B⟶C⟧ ⟹ (A⟶C)"
  by simp

lemma H1_4: "⟦A⟶(B⟶C);A⟶B⟧⟹(A⟶C)"
  by simp

除了可以用mp证明的第一条，其余三条在直觉逻辑IFOL中都没有证明。mp在IFOL中有实现。

反证法相关定理

经典逻辑与直觉逻辑最大的不同就是可以使用反证法了。

lemma H2_1: "¬¬A ⟹ A"
  by (rule notnotD)

lemma H2_2: "⟦(S⟹A) ⟹ B;(S⟹A) ⟹ ¬B⟧ ⟹ (S ⟹ ¬A)" 
  by auto

lemma H2_3: "A ⟹ ¬¬A"
  by (rule HOL.cnf.clause2raw_not_not)

lemma H2_4: "A⟹¬A ⟹ B"
  by (rule notE)

lemma H2_5: "A ⟹ (¬A ⟶ B)"
  by simp

lemma H2_6: "¬A ⟹ (A⟶B)"
  by simp

这几条中，notE在IFOL中有实现，其余都不能用于IFOL.

逆推相关定理

lemma H3_1: "(A⟶B) ⟹ (¬B ⟶ ¬A)"
  by (rule Set.not_mono)

lemma H3_2: "(A⟶¬B) ⟹ (B ⟶ ¬A)"
  by auto

lemma H3_3: "(¬A⟶B) ⟹ (¬B ⟶ A)"
  by auto

lemma H3_4: "(¬A ⟶ ¬B) ⟹ (B ⟶ A)"
  by auto

化简相关定理

lemma H4_1: "(¬A ⟶ A) ⟹ A"
  by (rule imp_elim)

lemma H4_2: "(A ⟶ ¬A) ⟹ ¬A"
  by(rule impCE)

lemma H4_3: "⟦(A⟶B); (A⟶¬B)⟧ ⟹ ¬A"
  by simp

lemma H4_4: "⟦(A⟶B); (¬A⟶B)⟧ ⟹ B"
  by auto

lemma H4_5: "¬(A⟶B) ⟹ A"
  by simp

lemma H4_6: "¬(A⟶B) ⟹ ¬B"
  by simp

合取相关定理

lemma H5_1: "A∧B ⟹ (A ⟹ B)"
  by(rule conjE)

lemma H5_2: "⟦A;B⟧ ⟹ A∧B"
  by (rule conjI)

lemma H5_3: "(A ∧ B) ⟹ (B ∧ A) "
  by simp

lemma H5_4: "(A∧B)∧C ⟹ A∧(B∧C)"
  by simp

lemma H5_5: "¬(A∧B) ⟹ (A⟶¬B)"
  by simp

lemma H5_6: "¬(A⟶B) ⟹ (A ∧ ¬B)"
  by (rule Meson.not_impD)

最后一个H5_6，也可以写成by meson:

lemma H5_6: "¬(A⟶B) ⟹ (A ∧ ¬B)"
  by meson

经典命题逻辑的公理推演系统

公理推演系统与自然推理系统是等价的，我们可以用公理推演系统的方法定义推理定理：

lemma Ax1: "A⟶(B⟶A)"
  by simp

lemma Ax2: "(A⟶(B⟶C)) ⟶ ((A⟶B)⟶(A⟶C))"
  by simp

lemma Ax3: "(¬A ⟶ B)⟶((¬A ⟶ ¬B)⟶A)"
  by simp

lemma Ax4: "A∧B ⟶ A"
  by simp

lemma Ax5: "A∧B ⟶ B"
  by simp

lemma Ax6: "A ⟶ (B⟶ A∧B)"
  by simp

lemma Ax7: "A⟶A∨B"
  by simp

lemma Ax8: "A ⟶ B∨A"
  by simp

lemma Ax9: "(A⟶C) ⟶ ((B⟶C)⟶(A∨B⟶C))"
  by auto

lemma Ax10: "(A⟷B)⟶(A⟶B)"
  by simp

lemma Ax11: "(A⟷B) ⟶ (B⟶A)"
  by simp

lemma Ax12: "(A⟶B) ⟶ ((B⟶A)⟶(A⟷B))"
  by auto

其中需要注意的是Ax9，在FOL中需要使用auto, simp无法识别，但在HOL中可以使用simp.

如何查找反例

不知道大家淹没在公式的海洋中的体验如何，反正我写的时候经常写出错误的公式来。
这时候我们需要的不是证明，而是先让系统帮我们搜索一下是不是有反例，我们的公式是不是写错了。

quickcheck

检查错误的第一个方法是使用quickcheck，直接当成语句写在IDE中即可。
比如Ax12被我们写错了，写成Ax12_2这样子：

lemma Ax12: "(A⟶B) ⟶ ((B⟶A)⟶(A⟷B))"
  by auto

lemma Ax12_2: "(A⟶B) ⟶ ((A⟶B)⟶(A⟷B))"
  quickcheck

系统就会给我们找一个反例：A=False, B=True

Testing conjecture with Quickcheck-exhaustive... 
Quickcheck found a counterexample:
  A = False
  B = True

quickcheck的结果会弹对话框，同时在output窗口显示出来：

quickcheck

nitpick

就像寻找定理证明方法可以用sledgehammer一样，检查反例也有专门的强大工具叫做nitpick。
用法和quickcheck一样，在定理后面写一句nitpick就好：

nitpick

nitpick作为专门的工具，配置项有很多，我们后面会详细介绍，这里大家先把它和quickcheck用起来。
如果公式已经错了，就不用为难sledgehammer去找证明了，先看看哪里写错了。

小结

不管是自然推理系统还是公理推演系统，在FOL和HOL证明定理时我们并不是用公理和推演规则进行推演的。公理和推演规则一般不对应FOL和HOL的公式，而是需要使用simp甚至auto进行证明的定理。
但是，我们还是可以按照我们在数理逻辑中所学的方法进行思考和推演，然后使用HOL的工具帮助我们简化推理的过程，尤其是nitpick等查错工具和sledgehammer等定理搜索工具。