Idrisで遊んでみた (2) — 自然数に関する命題の証明

前回は等号の証明に使える公理や規則(Idrisの組み込み関数)をいくつか紹介した。

これに加え、Idrisの標準ライブラリには自然数の性質に関する補題(?)がいくつか用意されている。そのうち、後で使う2つを紹介する。

一つ目は、和と後続者に関するものである。ペアノ算術にはちょうどこのような公理があったはずだ。plusSuccRightSucc

もう一つは、和の可換性である。ペアノ算術ではこれを証明するためには帰納法を使うが、証明(関数の実装)は標準ライブラリで用意されているので、ここではそれを使うだけにとどめておく。plusCommutative

さて、前回証明したいと言っていた命題は\[x=y+\mathtt{difference}\ p\]であった。ただし、\(p\) の表す命題は \(y\le x\), Idrisの型で言うと LTE y x である。この等式を証明するには、

differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)

という型の関数を実装すれば良い。

例によって場合分けする。

  • \(y=0\), つまり p=lteZero の場合:
    • この等式は自明に成り立つ。refl を返せば良い。
  • それ以外、つまり \(x=Sx’\), \(y=Sy’\), p=lteSucc p' の場合:
    • 帰納法の仮定として differenceP p' : x' = y' + difference p' が使える。
    • この仮定を使って S x' = (S y') + difference p' を示せば良い。(difference の定義を見れば difference p = difference p' なので、S x' = (S y') + difference p は自動的に導いてくれるようだ)
    • この仮定と、先に紹介した公理、補題を使って、自然演繹っぽい証明図を書くと、prooftree1となる。
    • この証明図にIdrisの項を書き加えるとprooftree1-tとなる。ただし、一部をアンダースコアで省略している。

これらをまとめて、Idrisの式として書けば

differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
differenceP lteZero = refl
differenceP {x = S x'} {y = S y'} (lteSucc p') = trans (trans (cong {f=S} (trans (differenceP p') (plusCommutative _ _))) (plusSuccRightSucc _ _)) (plusCommutative _ (S y'))

となる。一部の式をアンダースコアで省略しているが、最後の (S y') まで省略してしまうと処理系に怒られたので、そこは明示的に書いている。

今回は、自然演繹の証明図をCurry-Howard対応で翻訳することによって、命題を証明(関数を実装)した。等式の変形のところがやや煩雑になっているが、それはもとの自然演繹の証明図がそういうことになっていたことに起因するもので、Curry-Howard対応のせいでどうこうというものではない。

次回は量化子を含む命題を証明する予定である。Tacticを使った証明は筆者が不勉強なのでまだ扱わない。


コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です