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

第10节我们介绍了直觉一阶逻辑，它是不接受排中律的逻辑。在编程体感上，直觉一阶逻辑IFOL库，不支持auto，不支持sledgehammer，不能使用try0与try，基本上可以使用的就是simp或者手动推理。
simp是简化的意思，只做从左到右的等量代换来进行化简。它是auto中的一部分功能，但是auto要更强大一些。

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

经典一阶逻辑库FOL

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

theory fol2imports 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 simpfrom "1" "5" show ‹¬B ⟶ A› by simp
qed

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

proof (prove)
using this:¬ A ⟶ B¬ Agoal (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 simpwith "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 simpwith "1" show ‹¬B ⟶ A› by simp
qed

常用经典命题逻辑定理

蕴含相关定理

lemma H1_1 : "(A⟶B) ⟹ (A⟹B)"by(rule mp)lemma H1_2: "A ⟹ (B⟶A)"by simplemma H1_3: "⟦A⟶B; B⟶C⟧ ⟹ (A⟶C)"by simplemma 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 autolemma 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 simplemma 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 autolemma H3_3: "(¬A⟶B) ⟹ (¬B ⟶ A)"by autolemma 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 simplemma H4_4: "⟦(A⟶B); (¬A⟶B)⟧ ⟹ B"by autolemma H4_5: "¬(A⟶B) ⟹ A"by simplemma 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 simplemma H5_4: "(A∧B)∧C ⟹ A∧(B∧C)"by simplemma H5_5: "¬(A∧B) ⟹ (A⟶¬B)"by simplemma 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 simplemma Ax2: "(A⟶(B⟶C)) ⟶ ((A⟶B)⟶(A⟶C))"by simplemma Ax3: "(¬A ⟶ B)⟶((¬A ⟶ ¬B)⟶A)"by simplemma Ax4: "A∧B ⟶ A"by simplemma Ax5: "A∧B ⟶ B"by simplemma Ax6: "A ⟶ (B⟶ A∧B)"by simplemma Ax7: "A⟶A∨B"by simplemma Ax8: "A ⟶ B∨A"by simplemma Ax9: "(A⟶C) ⟶ ((B⟶C)⟶(A∨B⟶C))"by autolemma Ax10: "(A⟷B)⟶(A⟶B)"by simplemma Ax11: "(A⟷B) ⟶ (B⟶A)"by simplemma 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 autolemma Ax12_2: "(A⟶B) ⟶ ((A⟶B)⟶(A⟷B))"quickcheck

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

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

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

nitpick

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

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

小结

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