操作系統形式化驗證實踐教程(10) - 一階直覺邏輯

前面我們用了九講的篇幅把seL4驗證操作系統的地圖給大家迅速過了一遍，基礎好的同學已經可以基于前面的知識開始自己的工作了。
對于只學過離散數學，而沒學過專門數理邏輯的同學，我們稍微補充一點相關的知識。

我們在Isabelle中使用的一階邏輯主要是直覺主義的一階邏輯，當然我們也支持經典邏輯。

直覺主義邏輯

直覺主義邏輯intuitionistic logic的主要特點是不接受排中律，即要么命題為真或者為假。
也就是說，經典一階邏輯的定理：“P ∨ ?P”，在直覺主義邏輯中是不存在的。
直覺主義邏輯起源于布勞威爾Brouwer關于數學中構造性證明的研究。在構造性證明中不能使用反證法。直覺主義的主要原理是，通過構造性證明來建立數學命題的真。命題聯結詞的意義通過證明和構造來解釋：

$\alpha \wedge \beta$的證明由$\alpha$的證明和$\beta$的證明構成

$\alpha \vee \beta$的證明由$\alpha$的證明或者$\beta$的證明構成

$\alpha \to \beta$的證明是一個構造$\alpha$的每個證明都轉化為$\beta$的證明構成

$\perp$沒有證明

$?\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

總結

以上是生活随笔為你收集整理的操作系统形式化验证实践教程(10) - 一阶直觉逻辑的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。