コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

自然数の加法の交換法則 by Idris

これは「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 が全て消えて、これにて証明完了です。

ソースコード全体