操作系统形式化验证实践教程(10) - 一阶直觉逻辑
操作系统形式化验证实践教程(10) - 一阶直觉逻辑
前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍，基础好的同学已经可以基于前面的知识开始自己的工作了。
对于只学过离散数学，而没学过专门数理逻辑的同学，我们稍微补充一点相关的知识。
我们在Isabelle中使用的一阶逻辑主要是直觉主义的一阶逻辑，当然我们也支持经典逻辑。
直觉主义逻辑
直觉主义逻辑intuitionistic logic的主要特点是不接受排中律，即要么命题为真或者为假。
也就是说，经典一阶逻辑的定理："P ∨ ¬P"，在直觉主义逻辑中是不存在的。
直觉主义逻辑起源于布劳威尔Brouwer关于数学中构造性证明的研究。在构造性证明中不能使用反证法。直觉主义的主要原理是，通过构造性证明来建立数学命题的真。命题联结词的意义通过证明和构造来解释：
-
的证明由
的证明和
的证明构成
-
的证明由
-
的证明是一个构造
-
没有证明
-
的证明是一个构造使得对
这种证明解释，是布劳威尔、柯尔哥莫洛夫Kolmogorov和海廷Heyting提出的，也称为BHK解释。
直觉一阶逻辑编程
下面我们将能力限制到直觉一阶逻辑范围内，也就是我们只引入IFOL的库，我们向亚里士多德致敬，先来个三段论：
theory fol1
imports IFOL
begin
lemma mp2 : "⟦ P ⟹ Q; P⟧ ⟹ Q"
by (erule meta_mp)
end
by是apply和done的简写，如果写成apply...done的形式是这样:
lemma mp3 : "⟦ P ⟹ Q; P⟧ ⟹ Q"
apply(erule meta_mp, assumption)
done
这叫做mp规则，中文叫做肯定前件规则。
这么基础的逻辑问题，当然系统里早就有各种实现了，在最基础的Pure包中就有了：
proof (prove)
goal (1 subgoal):
1. (P ⟹ Q) ⟹ P ⟹ Q
Auto solve_direct: the current goal can be solved directly with
Pure.cut_rl:
(PROP ?psi ⟹ PROP ?theta) ⟹
PROP ?psi ⟹ PROP ?theta
Pure.meta_impE:
(PROP ?P ⟹ PROP ?V) ⟹
PROP ?P ⟹ (PROP ?V ⟹ PROP ?W) ⟹ PROP ?W
Pure.meta_mp:
(PROP ?P ⟹ PROP ?Q) ⟹ PROP ?P ⟹ PROP ?Q
Pure.revcut_rl:
PROP ?V ⟹ (PROP ?V ⟹ PROP ?W) ⟹ PROP ?W
不过，我们从HOL换成IFOL之后，发现能力比之前大大缩水了。我是特指工具自动化方面。
首先，by auto不能用了：
lemma mp2 : "⟦A⟹B;A⟧⟹B"
by auto
这个需要imports Main的情况下才能用，现在用不了了。
当然，在HOL环境条件下，系统推荐的规则也是不同的：
proof (prove)
goal (1 subgoal):
1. (A ⟹ B) ⟹ A ⟹ B
Auto solve_direct: the current goal can be solved directly with
Extraction.exE_realizer:
?P (snd ?p) (fst ?p) ⟹
(⋀x y. ?P y x ⟹ ?Q (?f x y)) ⟹
?Q (let (x, y) = ?p in ?f x y)
Extraction.exE_realizer':
?P (snd ?p) (fst ?p) ⟹ (⋀x y. ?P y x ⟹ ?Q) ⟹ ?Q
Hilbert_Choice.someI2:
?P ?a ⟹ (⋀x. ?P x ⟹ ?Q x) ⟹ ?Q (SOME x. ?P x)
Orderings.wellorder_class.LeastI2:
?P ?a ⟹ (⋀x. ?P x ⟹ ?Q x) ⟹ ?Q (Least ?P)
Orderings.wellorder_class.LeastI2_wellorder:
?P ?a ⟹
(⋀a. ?P a ⟹ ∀b. ?P b ⟶ a ≤ b ⟹ ?Q a) ⟹
?Q (Least ?P)
第二，神兵利器sledgehammer也不能用了：
no_atp.png
不过，受限之后对于我们学习基础知识还是很有好处的，这使我们能接触到系统中更基础的逻辑。
交与并
下面我们看一些基础的直觉命题逻辑：
交规则：
lemma conj_1 : "P∧Q⟹P"
by(erule conjunct1)
lemma conj_2 : "P∧Q⟹Q"
by(erule conjunct2)
并规则：
lemma disj_1: "P ⟹ P ∨ Q"
by(erule disjI1)
lemma disj_2: "Q ⟹ P ∨ Q"
by(erule disjI2)
并规则还可以更复杂一些：
lemma disj_E: "⟦P∨Q;P⟹R;Q⟹R⟧⟹R"
by(erule IFOL.disjE)
加上包名是用来强调下这是直觉一阶逻辑中的规则。
在HOL中，同样有等价的规则：
lemma disj_E: "⟦P∨Q;P⟹R;Q⟹R⟧⟹R"
by (erule HOL.disjE)
当然，在HOL中，我们直接by auto就好了：
lemma disj_E: "⟦P∨Q;P⟹R;Q⟹R⟧⟹R"
by auto
量词
全称量词：
lemma spec_2: "(∀x. P(x)) ⟹ P(x)"
by(erule allE)
针对全体元素的这个定理，有4条规则可以使用：
proof (prove)
goal (1 subgoal):
1. ∀x. P(x) ⟹ P(x)
Auto solve_direct: the current goal can be solved directly with
IFOL.allE: ∀x. ?P(x) ⟹ (?P(?x) ⟹ ?R) ⟹ ?R
IFOL.allE':
∀x. ?P(x) ⟹ (?P(?x) ⟹ ∀x. ?P(x) ⟹ ?Q) ⟹ ?Q
IFOL.all_dupE:
∀x. ?P(x) ⟹ (?P(?x) ⟹ ∀x. ?P(x) ⟹ ?R) ⟹ ?R
IFOL.spec: ∀x. ?P(x) ⟹ ?P(?x)
对于这么基础的功能，HOL中也是都有的：
proof (prove)
goal (1 subgoal):
1. ∀x. P x ⟹ P x
Auto solve_direct: the current goal can be solved directly with
HOL.allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R
HOL.allE': ∀x. ?P x ⟹ (?P ?x ⟹ ∀x. ?P x ⟹ ?Q) ⟹ ?Q
HOL.all_dupE:
∀x. ?P x ⟹ (?P ?x ⟹ ∀x. ?P x ⟹ ?R) ⟹ ?R
HOL.spec: ∀x. ?P x ⟹ ?P ?x
相等
我们可以学习下相等的可交换性的在IFOL中的证明：
lemma sym_2: "a=b ⟹ b=a"
apply(erule subst)
apply(rule refl)
done
我们也可以通过by的方式简写下：
lemma sym_3: "a=b ⟹ b=a"
by(erule subst, rule refl)
对于传递性，我们使用替换规则，加上假设：
lemma trans_2: "⟦ a=b; b=c⟧ ⟹ a=c"
apply(erule subst, assumption)
done
或者简写一下，假设不要了，直接by erule subst:
lemma trans_3: "⟦ a=b; b=c⟧ ⟹ a=c"
by(erule subst)
从系统的推荐来看，关于传递的规则还真不少：
proof (prove)
goal (1 subgoal):
1. a = b ⟹ b = c ⟹ a = c
Auto solve_direct: the current goal can be solved directly with
IFOL.back_subst: ?P(?a) ⟹ ?a = ?b ⟹ ?P(?b)
IFOL.basic_trans_rules(1): ?a = ?b ⟹ ?P(?b) ⟹ ?P(?a)
IFOL.basic_trans_rules(2): ?P(?a) ⟹ ?a = ?b ⟹ ?P(?b)
IFOL.basic_trans_rules(5): ?a = ?b ⟹ ?b = ?c ⟹ ?a = ?c
IFOL.forw_subst: ?a = ?b ⟹ ?P(?b) ⟹ ?P(?a)
对于不相等，我们可以借用上面的相等的定理：
lemma notsym_2: "a≠b ⟹ b ≠a "
apply(erule contrapos)
apply(erule sym_2)
done
对于HOL，直接上个simp，全搞定：
lemma sym_2: "a=b ⟹ b=a"
by simp
lemma notsym_2: "a≠b ⟹ b ≠a "
by simp
直觉逻辑
我们尝试证明lemma A9: "A ∨ ¬A"就会发现，并没有solve_direct的提示。
同样，两次求反，IFOL中也并没有solve_direct的证明：
lemma AA: "¬¬A ⟹ A"
而在HOL中，有HOL.notnotD: ¬ ¬ ?P ⟹ ?P是可以直接证明的。
HOL自动推理的几大利器
经过了IFOL手工的洗礼，再回头看HOL提供的自动工具，是不是有一种从古代穿越回现代的感觉。
从弱至强，HOL提供了几个级别的工具：
- solve_direct
- auto
- simp加上手动调整
- fastforce
- blast
- try0
- sledgehammer
- try
solve_direct是我们近期见的最多的，一般都会被自动提示。它是一个关键字，我们可以通过在代码中加入它来显示：
solve_direct.png
自动化方面，最基础的是auto，主要完成的工作是重写与化简，核心逻辑是simp:
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
apply (auto)
done
simp比起auto可以更加手动控制一些：
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
by(simp)
默认报错：
theorem iffI_2: (?P ⟹ ?Q) ⟹ (?Q ⟹ ?P) ⟹ ?P = ?Q
Failed to apply initial proof method⌂:
goal (1 subgoal):
1. (P ⟹ Q) ⟹ (Q ⟹ P) ⟹ P = Q
我们可以通过add:来增加规则，或者del:去删除规则。本例中，既然默认找不到，我们就simp add:一下：
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
by(simp add:iffI)
这样就顺利通过了。
比auto更强一些的是fastforce:
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
by(fastforce)
fastforce也可以加上simp add:来微调。
如果逻辑还更复杂，我们继续换更强的blast工具：
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
by(blast)
一般我们的一阶逻辑问题靠blast就可以解决了。
blast就不支持simp add:了。
如果blast还不灵，我们可以写一条try0语句来进行搜索：
try0.png
我们会看到搜索的结果：
Trying "simp", "auto", "blast", "metis", "argo", "linarith", "presburger", "algebra", "fast", "fastforce", "force", "meson", and "satx"...
Found proof: by blast (0 ms)
Found proof: by argo (0 ms)
Found proof: by linarith (1 ms)
Found proof: by fast (0 ms)
Found proof: by metis (2 ms)
Found proof: by fastforce (0 ms)
Found proof: by satx (0 ms)
Found proof: by auto (4 ms)
Found proof: by meson (1 ms)
Found proof: by force (3 ms)
Try this: by blast
(blast, argo, fast, fastforce, satx: 0 ms; linarith, meson: 1 ms; metis: 2 ms; force: 3 ms; auto: 4 ms)
根据搜到的结果抄一个吧，比如这个:
lemma iffI_2: "⟦P⟹Q;Q⟹P⟧ ⟹ P ⟷ Q"
by(argo)
从搜索结果也看到，只用simp是不行的。
最后的解决方案是try:
Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"...
Try0 found a proof: by blast (0 ms)
try不仁，以try0和sledgehammer等为刍狗。
参考文献
- 计算机科学中的现代逻辑学，王元元编著，北京：科学出版社，2001
- 结构证明论，马明辉编著，北京：科学出版社，2019
