操作系統(tǒng)形式化驗(yàn)證實(shí)踐教程(10) - 一階直覺邏輯

前面我們用了九講的篇幅把seL4驗(yàn)證操作系統(tǒng)的地圖給大家迅速過了一遍，基礎(chǔ)好的同學(xué)已經(jīng)可以基于前面的知識開始自己的工作了。
對于只學(xué)過離散數(shù)學(xué)，而沒學(xué)過專門數(shù)理邏輯的同學(xué)，我們稍微補(bǔ)充一點(diǎn)相關(guān)的知識。

我們在Isabelle中使用的一階邏輯主要是直覺主義的一階邏輯，當(dāng)然我們也支持經(jīng)典邏輯。

直覺主義邏輯

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

$\alpha \wedge \beta$的證明由$\alpha$的證明和$\beta$的證明構(gòu)成

$\alpha \vee \beta$的證明由$\alpha$的證明或者$\beta$的證明構(gòu)成

$\alpha \to \beta$的證明是一個構(gòu)造$\alpha$的每個證明都轉(zhuǎn)化為$\beta$的證明構(gòu)成

$\perp$沒有證明

$?\alpha$的證明是一個構(gòu)造使得對$\alpha$都得到$\perp$的證明。

這種證明解釋，是布勞威爾、柯爾哥莫洛夫Kolmogorov和海廷Heyting提出的，也稱為BHK解釋。

直覺一階邏輯編程

下面我們將能力限制到直覺一階邏輯范圍內(nèi)，也就是我們只引入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規(guī)則，中文叫做肯定前件規(guī)則。

這么基礎(chǔ)的邏輯問題，當(dāng)然系統(tǒng)里早就有各種實(shí)現(xiàn)了，在最基礎(chǔ)的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之后，發(fā)現(xiàn)能力比之前大大縮水了。我是特指工具自動化方面。

首先，by auto不能用了：

lemma mp2 : "?A?B;A??B"by auto

這個需要imports Main的情況下才能用，現(xiàn)在用不了了。

當(dāng)然，在HOL環(huán)境條件下，系統(tǒng)推薦的規(guī)則也是不同的：

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也不能用了：

不過，受限之后對于我們學(xué)習(xí)基礎(chǔ)知識還是很有好處的，這使我們能接觸到系統(tǒng)中更基礎(chǔ)的邏輯。

交與并

下面我們看一些基礎(chǔ)的直覺命題邏輯：

交規(guī)則：

lemma conj_1 : "P∧Q?P"by(erule conjunct1)lemma conj_2 : "P∧Q?Q"by(erule conjunct2)

并規(guī)則：

lemma disj_1: "P ? P ∨ Q"by(erule disjI1)lemma disj_2: "Q ? P ∨ Q"by(erule disjI2)

并規(guī)則還可以更復(fù)雜一些：

lemma disj_E: "?P∨Q;P?R;Q?R??R"by(erule IFOL.disjE)

加上包名是用來強(qiáng)調(diào)下這是直覺一階邏輯中的規(guī)則。

在HOL中，同樣有等價(jià)的規(guī)則：

lemma disj_E: "?P∨Q;P?R;Q?R??R"by (erule HOL.disjE)

當(dāng)然，在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條規(guī)則可以使用：

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)

對于這么基礎(chǔ)的功能，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

相等

我們可以學(xué)習(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)

對于傳遞性，我們使用替換規(guī)則，加上假設(shè)：

lemma trans_2: "? a=b; b=c? ? a=c"apply(erule subst, assumption)done

或者簡寫一下，假設(shè)不要了，直接by erule subst:

lemma trans_3: "? a=b; b=c? ? a=c"by(erule subst)

從系統(tǒng)的推薦來看，關(guān)于傳遞的規(guī)則還真不少：

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"就會發(fā)現(xiàn)，并沒有solve_direct的提示。

同樣，兩次求反，IFOL中也并沒有solve_direct的證明：

lemma AA: "??A ? A"

而在HOL中，有HOL.notnotD: ? ? ?P ? ?P是可以直接證明的。

HOL自動推理的幾大利器

經(jīng)過了IFOL手工的洗禮，再回頭看HOL提供的自動工具，是不是有一種從古代穿越回現(xiàn)代的感覺。

從弱至強(qiáng)，HOL提供了幾個級別的工具：

• solve_direct
• auto
• simp加上手動調(diào)整
• fastforce
• blast
• try0
• sledgehammer
• try

solve_direct是我們近期見的最多的，一般都會被自動提示。它是一個關(guān)鍵字，我們可以通過在代碼中加入它來顯示：

自動化方面，最基礎(chǔ)的是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)

默認(rèn)報(bào)錯：

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:來增加規(guī)則，或者del:去刪除規(guī)則。本例中，既然默認(rèn)找不到，我們就simp add:一下：

lemma iffI_2: "?P?Q;Q?P? ? P ? Q" by(simp add:iffI)

這樣就順利通過了。

比auto更強(qiáng)一些的是fastforce:

lemma iffI_2: "?P?Q;Q?P? ? P ? Q" by(fastforce)

fastforce也可以加上simp add:來微調(diào)。

如果邏輯還更復(fù)雜，我們繼續(xù)換更強(qiáng)的blast工具：

lemma iffI_2: "?P?Q;Q?P? ? P ? Q" by(blast)

一般我們的一階邏輯問題靠blast就可以解決了。
blast就不支持simp add:了。

如果blast還不靈，我們可以寫一條try0語句來進(jìn)行搜索：

我們會看到搜索的結(jié)果：

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)

根據(jù)搜到的結(jié)果抄一個吧，比如這個:

lemma iffI_2: "?P?Q;Q?P? ? P ? Q" by(argo)

從搜索結(jié)果也看到，只用simp是不行的。

最后的解決方案是try:

Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"... Try0 found a proof: by blast (0 ms)

try不仁，以try0和sledgehammer等為芻狗。

參考文獻(xiàn)

計(jì)算機(jī)科學(xué)中的現(xiàn)代邏輯學(xué)，王元元編著，北京：科學(xué)出版社，2001

結(jié)構(gòu)證明論，馬明輝編著，北京：科學(xué)出版社，2019

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。