操作系统形式化验证实践教程(10) - 一阶直觉逻辑

前面我们用了九讲的篇幅把seL4验证操作系统的地图给大家迅速过了一遍，基础好的同学已经可以基于前面的知识开始自己的工作了。
对于只学过离散数学，而没学过专门数理逻辑的同学，我们稍微补充一点相关的知识。

我们在Isabelle中使用的一阶逻辑主要是直觉主义的一阶逻辑，当然我们也支持经典逻辑。

直觉主义逻辑

直觉主义逻辑intuitionistic logic的主要特点是不接受排中律，即要么命题为真或者为假。
也就是说，经典一阶逻辑的定理：“P ∨ ¬P”，在直觉主义逻辑中是不存在的。
直觉主义逻辑起源于布劳威尔Brouwer关于数学中构造性证明的研究。在构造性证明中不能使用反证法。直觉主义的主要原理是，通过构造性证明来建立数学命题的真。命题联结词的意义通过证明和构造来解释：

α∧β\alpha\land\betaα∧β的证明由α\alphaα的证明和β\betaβ的证明构成
α∨β\alpha\lor\betaα∨β的证明由α\alphaα的证明或者β\betaβ的证明构成
α→β\alpha\to\betaα→β的证明是一个构造α\alphaα的每个证明都转化为β\betaβ的证明构成
⊥\perp⊥没有证明
¬α\lnot\alpha¬α的证明是一个构造使得对α\alphaα都得到⊥\perp⊥的证明。

这种证明解释，是布劳威尔、柯尔哥莫洛夫Kolmogorov和海廷Heyting提出的，也称为BHK解释。

直觉一阶逻辑编程

下面我们将能力限制到直觉一阶逻辑范围内，也就是我们只引入IFOL的库，我们向亚里士多德致敬，先来个三段论：

theory fol1imports 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 withPure.cut_rl:(PROP ?psi ⟹ PROP ?theta) ⟹PROP ?psi ⟹ PROP ?thetaPure.meta_impE:(PROP ?P ⟹ PROP ?V) ⟹PROP ?P ⟹ (PROP ?V ⟹ PROP ?W) ⟹ PROP ?WPure.meta_mp:(PROP ?P ⟹ PROP ?Q) ⟹ PROP ?P ⟹ PROP ?QPure.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 withExtraction.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) ⟹ ?QHilbert_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也不能用了：

不过，受限之后对于我们学习基础知识还是很有好处的，这使我们能接触到系统中更基础的逻辑。

交与并

下面我们看一些基础的直觉命题逻辑：

交规则：

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 withIFOL.allE: ∀x. ?P(x) ⟹ (?P(?x) ⟹ ?R) ⟹ ?RIFOL.allE':∀x. ?P(x) ⟹ (?P(?x) ⟹ ∀x. ?P(x) ⟹ ?Q) ⟹ ?QIFOL.all_dupE:∀x. ?P(x) ⟹ (?P(?x) ⟹ ∀x. ?P(x) ⟹ ?R) ⟹ ?RIFOL.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 withHOL.allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?RHOL.allE': ∀x. ?P x ⟹ (?P ?x ⟹ ∀x. ?P x ⟹ ?Q) ⟹ ?QHOL.all_dupE:∀x. ?P x ⟹ (?P ?x ⟹ ∀x. ?P x ⟹ ?R) ⟹ ?RHOL.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 withIFOL.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 = ?cIFOL.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 simplemma 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是我们近期见的最多的，一般都会被自动提示。它是一个关键字，我们可以通过在代码中加入它来显示：

自动化方面，最基础的是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语句来进行搜索：

我们会看到搜索的结果：

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