これは「Idris Advent Calendar 2020 - Qiita」の6日目の記事です。
Idris で自然数の加法の交換法則を証明してみましょう。
以下のように Comm.idr を書いて、ロードします。
関数comm
の型だけを書いた状態です。
%default total
はおまじないだと思ってください。
module Comm %default total comm : (x, y : Nat) -> x + y = y + x
$ idris ...... Idris is free software with ABSOLUTELY NO WARRANTY. For details type :warranty. Idris> :l Comm Type checking ./Comm.idr Holes: Comm.comm *Comm> :t comm x : Nat y : Nat -------------------------------------- comm : plus x y = plus y x Holes: Comm.comm *Comm>
:l Comm
でモジュールをロードしています。
:t comm
で関数comm
の型を確認しています。
これで型定義が確認できました。
自然数の定理の証明方法として、
引数の自然数をZ(0)
とS(+1)
に分ける、という方法があります。
今回は引数が2つあるので、4パターンに分けられます。やってみましょう。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = ?rhs1 comm (S x) Z = ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2, Comm.rhs1 *Comm> :t rhs1 -------------------------------------- rhs1 : 0 = 0 Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2, Comm.rhs1 *Comm>
?rhs1
というのは Hole です。?
の後の文字列は何でも良いです。
Idris では、分からない部分は Hole にしておいて、とりあえずロードする事ができます。
Hole を:t
すると、その部分の型を示してくれます。
(Z, Z)の場合
フライングで出ちゃってますが、Hole rhs1 の型は0 = 0
でした。
両辺の値が等しい時は、Refl
が使えます。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
Hole が一つ減りましたね。
(S x, Z)の場合
*Comm> :t rhs2 x : Nat -------------------------------------- rhs2 : S (plus x 0) = S x Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
Hole rhs2 の型はこのようになっています。
x + 0 = x ですから、この部分を計算したいですね。
標準ライブラリを探すと、plusZeroRightNeutral
という関数があるので、これを使います。
また、「rewrite」という構文を使います。
ある式に対して、等式を持ってきて、ある式の中で左辺に該当する部分を右辺に置き換えます。
エディタで置換するようなものです。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in ?rhs2 comm Z (S y) = ?rhs3 comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm> :t rhs2 x : Nat _rewrite_rule : plus x 0 = x -------------------------------------- rhs2 : S x = S x Holes: Comm.rhs4, Comm.rhs3, Comm.rhs2 *Comm>
おおお、左辺と右辺が一致しましたね。これでRefl
が使えます。
(Z, S y)の場合
この場合もさっきとほぼ同じなので、同様に処理します。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4 *Comm>
Hole は残り一つです。
(S x, S y)の場合
*Comm> :t rhs4 x : Nat y : Nat -------------------------------------- rhs4 : S (plus x (S y)) = S (plus y (S x)) Holes: Comm.rhs4 *Comm>
複雑ですね。
このような場合は、plus
の中にあるS
を、外へはじき出せないか考えてみましょう。
再び標準ライブラリから、plusSuccRightSucc
という関数を探し出します。
*Comm> :t plusSuccRightSucc plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right Holes: Comm.rhs4 *Comm>
いけそう...ですが、左辺と右辺が逆ですね。このような場合は、関数sym
をかましましょう。
S
を外へはじく箇所は二つあるので、二回連続で rewrite します。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = rewrite sym (plusSuccRightSucc x y) in rewrite sym (plusSuccRightSucc y x) in ?rhs4
*Comm> :l Comm Type checking ./Comm.idr Holes: Comm.rhs4 *Comm> :t rhs4 x : Nat y : Nat _rewrite_rule : plus x (S y) = S (plus x y) _rewrite_rule1 : plus y (S x) = S (plus y x) -------------------------------------- rhs4 : S (S (plus x y)) = S (S (plus y x)) Holes: Comm.rhs4 *Comm>
おしい! x と y が逆です。
でもあきらめてはいけません。実はもう解けているのです。
hoge : x -> T x を証明したい時、
hoge Z と
hoge (S x) に分けたとすると、
hoge (S x) のところでは、hoge x が使えるのです。
定理証明の分野でも、再帰は有効なのです。
今回の場合だと、(comm x y)(型はx + y = y + x)
が使えます。
最後に、両辺にS S
がかかっていますが、これには関数cong
を使います。
関数cong
と、{}で囲む暗黙の引数については、今回は説明しません。
comm : (x, y : Nat) -> x + y = y + x comm Z Z = Refl comm (S x) Z = rewrite plusZeroRightNeutral x in Refl comm Z (S y) = rewrite plusZeroRightNeutral y in Refl comm (S x) (S y) = rewrite sym (plusSuccRightSucc x y) in rewrite sym (plusSuccRightSucc y x) in cong {f = S . S} (comm x y)
*Comm> :l Comm Type checking ./Comm.idr *Comm>
Hole が全て消えて、これにて証明完了です。
ソースコード全体