Lean4で命題論理の自動証明をする
はじめに
これは定理証明支援系 Advent Calendar 2023の記事です。
前回lean4-logicにおけるGödelの第一不完全性定理の証明について書きました。今回もlean4-logicで簡単な自動証明を実装したのでそれについて書きます。
メタプログラミング
CoqやIsabelle, Agdaなど証明支援言語には種類が色々ありますが、中でもLeanはメタプログラミングが強力で書きやすい印象があります。その例としてここでは命題論理の自動証明の実装を行います[1]。lean4-metaprogramming-bookという資料があり、このようなプログラムを書くうえでは参考になります。
Leanのメタプログラミングにおいて、項、型、命題、証明や関数といったオブジェクトは型Exprによって記述されます。したがって今回のような自動証明を行いたいならば、ゴールの命題を意味するExprを受け取って証明を意味するExprを帰すような関数を定義すればよいだけです。ただし、これを素朴に行うのはかなり困難で、というのもすべての型がExprなので型のない言語でプログラミングをしているのに近く、加えて型クラスやinplicit argumentなどの特殊な項がよく現れるためバグが頻出します。このようにExprを生のまま扱うのは大変なので、一度別の項に変換してから証明探索などの処理を行うことにします。例えば以下は型Fの論理式を意味するExpr[2]を型Lit Fに変換する関数です。
partial def denote : Q($F) → MetaM (Lit F)
| ~q(⊤) => return ⊤
| ~q(⊥) => return ⊥
| ~q($p ⋏ $q) => return (←denote p) ⋏ (←denote q)
| ~q($p ⋎ $q) => return (←denote p) ⋎ (←denote q)
| ~q($p ⟶ $q) => return (←denote p) ⟶ (←denote q)
| ~q($p ⟷ $q) => return (←denote p) ⟷ (←denote q)
| ~q(~$p) => return ~(←denote p)
| ~q($e) => return atom e
ここでExprに（完全ではないが）ある程度型をつけてくれるquote4を用いています。これはExprの場合分けを（返り値はモナドに包まれますが）行ってくれるため便利です。
Lit FをExprに変換する関数は以下のとおりです。
abbrev toExpr : Lit F → Q($F)
| atom e => q($e)
| ⊤ => q(⊤)
| ⊥ => q(⊥)
| p ⋏ q => q($(toExpr p) ⋏ $(toExpr q))
| p ⋎ q => q($(toExpr p) ⋎ $(toExpr q))
| ~p => q(~$(toExpr p))
| p ⟶ q => q($(toExpr p) ⟶ $(toExpr q))
証明探索
一階論理の完全性定理の証明はTait計算の証明探索で行いましたが、ここで扱う型Fの論理式は~~p = pなどの性質が成り立たない可能性もあるため、Gentzen流の推件計算の証明探索を行います。具体的にはFは以下を満たすような関係_ ⊢ᴳ _を持っていることを要求します。
class Gentzen (F : Type u) [LogicSymbol F] extends TwoSided F where
verum (Γ Δ : List F) : Γ ⊢ᴳ ⊤ :: Δ
falsum (Γ Δ : List F) : ⊥ :: Γ ⊢ᴳ Δ
negLeft {p : F} {Γ Δ : List F} : Γ ⊢ᴳ p :: Δ → ~p :: Γ ⊢ᴳ Δ
negRight {p : F} {Γ Δ : List F} : p :: Γ ⊢ᴳ Δ → Γ ⊢ᴳ ~p :: Δ
andLeft {p q : F} {Γ Δ : List F} : p :: q :: Γ ⊢ᴳ Δ → p ⋏ q :: Γ ⊢ᴳ Δ
andRight {p q : F} {Γ Δ : List F} :
Γ ⊢ᴳ p :: Δ → Γ ⊢ᴳ q :: Δ → Γ ⊢ᴳ p ⋏ q :: Δ
orLeft {p q : F} {Γ Δ : List F} :
p :: Γ ⊢ᴳ Δ → q :: Γ ⊢ᴳ Δ → p ⋎ q :: Γ ⊢ᴳ Δ
orRight {p q : F} {Γ Δ : List F} : Γ ⊢ᴳ p :: q :: Δ → Γ ⊢ᴳ p ⋎ q :: Δ
implyLeft {p q : F} {Γ Δ : List F} :
Γ ⊢ᴳ p :: Δ → q :: Γ ⊢ᴳ Δ → (p ⟶ q) :: Γ ⊢ᴳ Δ
implyRight {p q : F} {Γ Δ : List F} : p :: Γ ⊢ᴳ q :: Δ → Γ ⊢ᴳ (p ⟶ q) :: Δ
wk {Γ Γ' Δ Δ' : List F} : Γ ⊢ᴳ Δ → Γ ⊆ Γ' → Δ ⊆ Δ' → Γ' ⊢ᴳ Δ'
em {p} {Γ Δ : List F} (hΓ : p ∈ Γ) (hΔ : p ∈ Δ) : Γ ⊢ᴳ Δ
class LawfulGentzen (F : Type u) [LogicSymbol F] [System F]
extends Gentzen F where
toProof₁ {Γ} {T : Set F} {p : F} : Γ ⊢ᴳ [p] → (∀ q ∈ Γ, T ⊢ q) → T ⊢ p
これは明らかに古典命題論理や古典n階論理に成立します。また（古典的な）様相論理や認識論理においても成立するため、将来的にこのような論理を定義した際にもこの自動証明を適用できます。
自動証明
定義した自動証明はtautology, prover [...]タクティックによって呼び出すことが可能です。具体的に証明を構成させる命題を証明させようとすると（lean4-logicではT ⊢ p）かなり時間がかかりますが、単に証明可能性（T ⊢! p）を示す場合ならば、複雑な論理式でも割と高速に自動証明ができます。
example : T ⊢! p ⋎ q ⋎ r ⋎ s ⟷ r ⋎ p ⋎ s ⋎ q ⋎ p := by tautology
example : T ⊢! p ⟷ p ⋎ p ⋎ p ⋎ p ⋎ p ⋎ p ⋎ p := by tautology
example : T ⊢! ((p ⟶ q) ⟶ p) ⟶ p := by tautology
example : T ⊢! (r ⟶ p) ⟶ ((p ⟶ q) ⟶ r) ⟶ p := by tautology
example : T ⊢! (~p ⟶ p) ⟶ p := by tautology
example : T ⊢! (p ⟶ q) ⋎ (q ⟶ p) := by tautology
example : T ⊢! (p ⟷ q) ⟷ (~q ⟷ ~p) := by tautology
example (h : T ⊢! p ⟷ q) : T ⊢! ~q ⟷ ~p := by prover [h]
example (h : T ⊢! p ⟷ q) (hp : T ⊢! p) : T ⊢! q := by prover [h, hp]
Discussion