はじめに
Coq と似た後発の定理証明支援に LEAN というのがあって、VSCode上でやるならかなり快適。少し入門してみたので、簡単に証明できるいつものやつ、つまり 排中律 ⇔ 二重否定除去 などを証明しながらCoqとの違いを感じてみます。
ざっくりいって Lean4 は Coq とおなじ CIC のための道具で、
- Coqのようにタクティックでの証明もできるし
- Agdaのように対話的に直接証明項を構成できるし
- それらを一つの証明の中で混ぜながらもできる
- UTF8 を使った多彩な記号を使った syntax でみやすい
といったなかなかイケてる仕様であり、少し触っただけでもVSCodeの補完・Copilot機能とあいまってかなり快適に定理証明ができそうだという感触をもちました
本文
まずは排中律とかを定義してみます:
def EM := forall (P:Prop), P ∨ ¬P
def DNE := forall (P:Prop), ¬¬P → P
def MORGAN4 := forall (P Q:Prop), ¬(¬P ∧ ¬Q) -> P ∨ Q
def PEIRCE := forall (P Q:Prop), ((P → Q) → P) → P
def IMPLCASE:= forall (P Q:Prop), (P → Q) → ¬P ∨ Q
この5つの同値性を証明しながら Lean らしさをさがしてみます。タクティックを使う証明はCoqとあまり変わらないので、証明項を直接構成してみます。
まず EM↔IMPCASE をみてみます:
theorem em_impcase_iff : EM ↔ IMPLCASE := ⟨
(fun (em:EM) P Q (h: P→ Q) => show (¬P ∨ Q) from
match (em P) with
| Or.inl hp => Or.inr (h hp)
| Or.inr hnp => Or.inl hnp)
,
(fun (h: IMPLCASE) P => show (P ∨ ¬P) from
Or.comm.mp (h P P id))
⟩
軽く説明です:
-
Iffは単一のコンストラクタのみを持つのでLeanの anonymous constructor とよばれる ⟨ h1 , h2 ⟩ という形で書くことができます。一つ目が⇒の証明項、二つ目が⇐の証明項です。
-
⇒の証明: いわゆる intros タクティックに相当する fun によるラムダ抽象をし終わったあとのGoalを show でアノテートすることで可読性をあげています（なくても通ります）。排中律のおかげで P∨¬P の証明項が得られるので場合分けで分析できます。一つ目のブランチでは P を仮定して証明項を構成し、二つ目のブランチでは ¬P を仮定して証明項を構成します。matchを使いましたが Or.elim のような除去則を使っても同じです。
-
⇐の証明：IMPCASEのQにPを代入すると即座に¬P∨Pが得られるのでOr.commでひっくり返してできあがりです。P→Pの証明項は 恒等関数 id です。
続いて EM->DNE,DNE->MORGAN4,MORGAN4->EM というループからこの3つが同値であることを示します:
theorem em_imp_dne : EM → DNE := fun (em: EM) (P: Prop) (h: ¬¬P) =>
show P from Or.elim (em P) id (fun hnp => absurd hnp h)
theorem dne_imp_morgan4 : DNE → MORGAN4 := fun (dne: DNE) (P Q: Prop) (h: ¬(¬P ∧ ¬Q)) =>
suffices h1: ¬¬(P ∨ Q) from (dne _ h1)
fun h2 => h ⟨(fun hp => h2 (Or.inl hp)), (fun hq => h2 (Or.inr hq))⟩
theorem morgan4_imp_em : MORGAN4 → EM := fun (m4: MORGAN4) (P: Prop) =>
have h: ¬(¬P ∧ ¬¬P) := fun h1 => h1.right (fun hp => h1.left hp)
m4 P (¬P) h
- 1つめ: 先ほどは match を使いましたが今回は Or.elim という除去則を使っています。やることは同じです
- 2つめでは suffices ? from ? をつかっています。これはCoqでいうところの enough タクティックです。二重否定が得られれば二重否定除去からすぐにGoalがえられるので、問題はこの二重否定をどう構成するかです。否定なので 1回だけ intro すなわちラムダ抽象ができ、 ¬(P ∨ Q) をコンテキストに加えて False がGoalになります。そこでコンテキストの ¬(¬P ∧ ¬Q)) にapply すれば結局 ¬P ∧ ¬Q を示せばよいとわかります。Andは単一のコンストラクタをもつので前述の anonymous constructor の記法が使えます
- 3つめでは have を使っています。これは Coq での assert タクティックと同じでサブゴールを設定するものです。タクティックをつかった後ろからの推論ではなく、順繰りの人間にわかりやすい推論を提供できます。もちろんこれも suffices を使ってもよかったですし、どちらも使わないこともできました
Iff の証明は自明です:
theorem em_dne_iff : EM ↔ DNE := ⟨ em_imp_dne,
fun (dne: DNE) => morgan4_imp_em (dne_imp_morgan4 dne)⟩
theorem em_morgan4_iff : EM ↔ MORGAN4 :=
⟨(fun (em:EM) => dne_imp_morgan4 (em_imp_dne em)),
morgan4_imp_em ⟩
最後にパースの法則がらみの証明です
theorem peirce_imp_dne : PEIRCE → DNE := fun (peirce: PEIRCE) (P: Prop) (hnnp: ¬¬P) =>
peirce P False (fun h: P → False => absurd h hnnp)
theorem em_imp_peirce : EM → PEIRCE := fun (em: EM) (P Q: Prop) (h: (P → Q) → P) =>
Or.elim (em P) id (fun hnp => h (fun hp => absurd hp hnp ))
theorem em_peirce_iff : EM ↔ PEIRCE := Iff.intro
em_imp_peirce
(fun (peirce: PEIRCE) => morgan4_imp_em (dne_imp_morgan4 (peirce_imp_dne peirce)))
特に新しい要素は出せませんでした
さいごに
タクティックによる証明は自動化しやすいのですが、いかんせん読みずらすぎます。だからといって直接証明項を構成するのも、少し複雑になった言明に対しては複雑になりすぎます。この中間あたりが私にとっては一番居心地がよく、LEANとエディタによる支援という環境はかなり心地が良いです。もう少しLeanを触っていこうかなとおもいます。みなさまもぜひどうぞ。