Open2023/07/08にコメント追加5

Lean4勉強メモ

lean4

グミ

Lean 4の勉強メモを記します。可能であれば、私がある程度理解しているHaskellと比較してみます。

Hello, world!

Lean4

test.lean

def main : IO Unit := IO.println "Hello, world!"

ターミナル

> lean --run .\test.lean
Hello, world!

Haskell

test.hs

main :: IO ()
main = putStrLn "Hello, world!"

グミ

入力した文字列を受け取って挨拶するコードを書いてみた。本当は下のコードでHello, John!と表示されてほしかったが、getLineだと改行まで含まれてしまうようで、意図しない結果になった。

Main.lean

def main : IO Unit := do
 IO.print "name: "
 let stdin ← IO.getStdin
 let input ← stdin.getLine
 IO.println s!"Hello, {input}!"

ターミナル

> lean --run .\Main.lean
name: John
Hello, John
!
>

グミ

String.dropRightWhileとChar.isWhitespaceを使えば良いことがわかった。
というか、公式チュートリアルに普通に書いてあった。

これで文字列の末尾からスペース・タブ・改行コードを除くことができる。

Main.lean

def main : IO Unit := do
 IO.print "name: "
 let stdin ← IO.getStdin
 let input ← stdin.getLine
 let name := input.dropRightWhile Char.isWhitespace
 IO.println s!"Hello, {name}!"

> lean --run .\Main.lean
name: John
Hello, John!
>

グミ

排中律の二重否定の証明

Lean4は基本的には直観主義論理（構成的論理）なので、そのままでは排中律（the law of excluded middle）は証明できません。名前空間Classicalを用いると、排中律等の古典論理の法則を利用できます。^[1]

一方で、排中律の二重否定は直観主義論理で証明できるらしいので、今回はその証明に挑戦してみました。

Main.lean

theorem double_negate_excluded_middle (p : Prop) : ¬¬(p ∨ ¬ p) :=
  fun nem : ¬(p ∨ ¬p) => show False from nem (
    Or.inr (fun hp : p => show False from (nem (Or.inl hp)))
  )

#print double_negate_excluded_middle

日本語で書き下すと、以下のような感じです。

定理（排中律の二重否定）
任意の命題 $p$ について、 $\neg\neg(p \lor \neg p)$ が成り立つ。

証明
$\neg(p \lor \neg p)$ を仮定して、矛盾を導く。
まず、 $\neg p$ を導く。
そのために、 $p$ を仮定して矛盾を導く。
仮定 $p$ より、 $p \lor \neg p$ が成り立つが、仮定 $\neg(p \lor \neg p)$ より矛盾する。
$p$ を仮定して矛盾を導いたので、 $\neg p$ が成り立つ。
$\neg p$ より、 $p \lor \neg p$ が成り立つが、仮定 $\neg(p \lor \neg p)$ より矛盾する。
$\neg(p \lor \neg p)$ を仮定して、矛盾を導いたので、 $\neg\neg(p \lor \neg p)$ が成り立つ。 $\square$

Lean4のコードの最後に#print double_negate_excluded_middleと書きましたが、これによって、VS Codeの右側（Lean Infoview）に定理の証明が表示されるようです。

Lean Infoview

All Messages (1)
Main.lean:6:0
theorem double_negate_excluded_middle : ∀ (p : Prop), ¬¬(p ∨ ¬p) :=
fun p nem =>
  let_fun this :=
    nem
      (Or.inr fun hp =>
        let_fun this := nem (Or.inl hp);
        this);
  this

自分で書いたものとは少し違う証明が表示されました。

感想

Lean4、直観主義論理の良い練習となりました。

脚注

Propositions and Proofs - Theorem Proving in Lean 4 ↩︎

グミ

tactic-styleでも書いてみた。

Main.lean

theorem double_negate_excluded_middle (p : Prop) : ¬¬(p ∨ ¬p) := by
 intro h1
 apply h1
 apply Or.inr
 intro h2
 apply h1
 apply Or.inl
 assumption