Zenn
🍩

Idrisで定理証明をやっていく - 論理式 AND

2021/12/12に公開
#
idris
#
定理証明
tech

論理式

まずやっていくのは命題論理です。
（変数としては命題しかない論理）

命題論理の論理式は、以下のように定義されるようです。

  1. アルファベット大文字で命題を表す
  2. 命題Pがあったとき、Pは正しい論理式
  3. 論理式Aがあったとき否定（￢A）も論理式
  4. 論理式A、Bがあったとき (A 特定の演算子 B) も論理式
    演算子の種類
    • かつ、and、∧
    • または、or、∨
    • ならば、→

上記の繰り返しで生成できるものを命題論理の論理式とします。（Wikipedia読みました）
なお、カッコを外しても意味が変わらない場合はもちろん外してよいです。

やっていく

否定はちょっと難しいので今回はandからやっていきます。

論理学は記号のとっつきづらさで損してる気がしてるので、論理学っぽい記号はあまり使わない方向でやっていきます。

また、定理証明をプログラムでやるときみんな英語で書くのが普通ですが、かなり読みづらいので、日本語は積極的に使っていきます。
「交換則という言葉は知っているがローマ字で書くのはダサいし、英語で何というか分からない。調べて分かったけど全然ピンとこない。。」みたいなことが多発するので、それだったら日本語使ったほうがいいと思います。

A and B

Idrisでは、A and Bという命題の型は、タプルを使って (A, B) と表します。
タプルを作れるということは、同時にAもBも値が存在する（証明が存在する）ということだからです。
タプルだとパターンマッチもできるし、3つも4つも要素をかけるので便利です。

まずは簡単に成り立ちそうな、A and B ならば B and A を証明しましょう。

証明（関数）の型を、そのまま書きます。
（見た目分かりやすいよう関数名を日本語にしましたが、作っているときは f とかの適当な名前のほうがやりやすいです。）

and交換則 : (A, B) -> (B, A)

この状態でコンパイルして、文法が正しいことと、関数定義がないと怒られることを確認します。

関数（証明）の中身を書いていきます。
(A, B)という型（命題）の変数（命題が正しい証拠）を受け取って、そこから(B, A)を作り出せれば、それが証明になります。

(A, B)から(B, A)を作るには、(A, B)を引数のパターンマッチで受け取ってひっくり返せばいいです。

%default total -- 証明の網羅性チェックする設定。プログラム先頭に書く。

and交換則 : (A, B) -> (B, A)
and交換則 (a, b) = (b, a)

main : IO ()
main =
  putStr "Q.E.D."

コンパイルして怒られなければ証明完了です。

練習問題

((A and B) and (B and C)) ならば (A and B and C)

Discussion