はじめに

今年は生成AIが飛躍的に成長する一年でしたね。プログラミングも生成AIがやれるようになって、人が書くプログラムは工芸、民芸のようになっていくのではないでしょうか。日頃からプログラミングを労働ではなく芸術活動としてやっていきたいものです。

ということで、僕が美しい言語だと思っている Idris の話を書きます。

前提

Idris のバージョンは 1.3.4 を使っています¹。
brew install idris でインストールしよう！

どんな話？

replace、 rewrite という2つの関数/マクロについて使い方を説明する、という話です。

Idrisで複雑な証明を書く時にはほぼ必ず使う上に、コツを掴むまでは難しいという初心者にとっての壁のようなヤツらです。

目標

「任意の自然数 n に対し、 n * 2 = n + n である」という命題を証明するのを今回の目標としましょう。

方針

まずは数学的に証明を考えてみましょう。

a. 2 と + の定義から、 2 = 1 + 1
b. 分配法則より、 n * (1 + 1) = n * 1 + n * 1
c. 1 は * において単位元であるから、 n * 1 = n
d. 以上から、 n * 2 = n * (1 + 1) = n * 1 + n * 1 = n + n

厳密にはそれぞれもっと深掘りできますが、まあこれで良さそうです。

それぞれ Idris での表現を考えてみましょう。

a. 2 = 1 + 1

これは Idris においても「定義より明らか」となります。

Idris における自然数 2 の定義は S (S Z) です。 S は後者関数、 Z は 0 を表しています(なので 1 は S Z)。

また、Idris における自然数の足し算 plus の定義は以下となっています:

plus : (n, m : Nat) -> Nat
plus Z right        = right
plus (S left) right = S (plus left right)

従って、 1 + 1 = (S Z) + (S Z) = S (S Z) = 2 となり、定義から 1 + 1 = 2 が言えます。
この関数は total なので、型に 1 + 1 と書いても計算されて 2 として扱われることになります。

b. 分配法則より、 n * (1 + 1) = n * 1 + n * 1

標準ライブラリである Prelude に、分配法則を表す関数 multDistributesOverPlusRight があります。この関数の型を簡略化して書くと、

multDistributesOverPlusRight: (a, b, c: Nat) -> a * (b + c) = a * b + a * c

となります。これに n, 1, 1 を渡せば

multDistributesOverPlusRight n 1 1: n * (1 + 1) = n * 1 + n * 1

となりますね。型における 1 + 1 は計算されて 2 になるため、実際には

multDistributesOverPlusRight n 1 1: n * 2 = n * 1 + n * 1

となります。

c. 1 は * において単位元であるから、 n * 1 = n

これも Prelude に関数 multOneRightNeutral というのがあります。この関数の型を簡素化して書くと、

multOneRightNeutral: (a: Nat) -> a * 1 = a

です。なので、これに n を渡せば

multOneRightNeutral n: n * 1 = n

となりますね。

d. 以上から、 n * 2 = n * (1 + 1) = n * 1 + n * 1 = n + n

ここが今回の肝です。ここでは「式の一部を等しいもので置き換えても同じ」という事実が暗に使われています。

これを表現するのが replace という関数、あるいは rewrite というマクロです。
replace の型を見てみると:

Idris> :t replace
replace : (x = y) -> P x -> P y

命題として翻訳すると「x とｙが等しいとき、P(x) が成り立つならば P(y) が成り立つ」ですね。
これを先ほどの言い方に直すと

「x と y が等しいならば、 P(x) という命題の中の x を y に置き換えても成り立つ」

となります。ここまでで

multDistributesOverPlusRight n 1 1: n * 2 = n * 1 + n * 1
multOneRightNeutral n: n * 1 = n

という2つの事実が示せているので、

「n * 1 = n なので、 n * 2 = n * 1 + n * 1 の中の n * 1 を n に置き換えても成り立つ」

という議論が成立するはずです。先ほどの文言と見比べると

x = n * 1, y = n, P(x) = (n * 2 = x + x)

とすれば良いことがわかります。この x, y, P は replace の implicit な引数なので、{} を使って指定する必要があります:

replace
  {x = n * 1}
  {y = n}
  {P = \x => n * 2 = x + x}
  (multOneRightNeutral n)              -- x = y, すなわち n * 1 = n
  (multDistributesOverPlusRight n 1 1) -- P x  , すなわち n * 2 = n * 1 + n * 1

以上、まとめると:

twiceIsDouble: (n : Nat) -> n * 2 = n + n
twiceIsDouble n =
  replace
    {x = n * 1}
    {y = n}
    {P = \x => n * 2 = x + x}
    (multOneRightNeutral n)
    (multDistributesOverPlusRight n 1 1)

これでひとまずは証明完了です。

`rewrite`

replace を使った証明では、x, y, P の3つを明示的に指定する必要があり、割とめんどい形になっていました。

これを解決できるのが rewrite です。こちらは関数ではなくマクロなため、定義を読んで理解するのはなかなか難しいと思います。

rewrite は hole の型の中の x を、 x = y を使って y に置き換えるもの と考えると良いです。

`rewrite` で書き直す

rewrite を使って、もう一度最初から証明をやり直してみましょう。今度はTDDに則って、型から始めます:

twiceIsDouble' : (n : Nat) -> n * 2 = n + n

「任意の自然数 n に対し、 n * 2 = n + n が成り立つ」という命題を型にしました。
続いて、TDDの流れに沿って定義句を自動生成してもらいます:

twiceIsDouble' : (n : Nat) -> n * 2 = n + n
twiceIsDouble' n = ?twiceIsDouble'_rhs

?twiceIsDouble'_rhs という hole ができました。REPLでこの型を見てみましょう:

Idris> :l twiceIsDouble.idr -- REPLからファイルを読み込む
Holes: Main.twiceIsDouble'_rhs

*twiceIsDouble> :t twiceIsDouble'_rhs
  n : Nat
--------------------------------------
twiceIsDouble'_rhs : mult n 2 = plus n n

mult と plus が使われていますが、 n * 2 = n + n と同じですね。

ここで、この型に登場する n * 2 を、 n * 1 + n * 1 に置き換えます。

n * 2 = n * 1 + n * 1 という型の値として multDistributesOverPlusRight n 1 1 があったので、これを利用して、

twiceIsDouble' : (n : Nat) -> n * 2 = n + n
twiceIsDouble' n = rewrite multDistributesOverPlusRight n 1 1 in ?twiceIsDouble'_rhs

rewrite は rewrite (x = y 型の値) in (hole の型が書き換わったもの) という形で使います。新しい hole の型を見てみましょう:

*twiceIsDouble> :r -- ファイルを更新したのでリロードする
Holes: Main.twiceIsDouble'_rhs

*twiceIsDouble> :t twiceIsDouble'_rhs
  n : Nat
  _rewrite_rule : mult n 2 = plus (mult n 1) (mult n 1)
--------------------------------------
twiceIsDouble'_rhs : plus (mult n 1) (mult n 1) = plus n n
Holes: Main.twiceIsDouble'_rhs

n * 1 + n * 1 = n + n という型に変わっていますね！

ここでさらに n * 1 = n を利用して、 n * 1 を n に置き換えます。 n * 1 = n の値としては multOneRightNeutral n がありました:

twiceIsDouble' : (n : Nat) -> n * 2 = n + n
twiceIsDouble' n =
  rewrite multDistributesOverPlusRight n 1 1 in
  rewrite multOneRightNeutral n in
  ?twiceIsDouble'_rhs

改行とインデントを追加していますが、hole だった箇所を rewrite multOneRightNeutral n in ?twiceIsDouble'_rhs に変えています。

新しくなった hole の型を見てみましょう:

*twiceIsDouble> :r
Holes: Main.twiceIsDouble'_rhs

*twiceIsDouble> :t twiceIsDouble'_rhs
  n : Nat
  _rewrite_rule : mult n 2 = plus (mult n 1) (mult n 1)
  _rewrite_rule1 : mult n 1 = n
--------------------------------------
twiceIsDouble'_rhs : plus n n = plus n n
Holes: Main.twiceIsDouble'_rhs

n + n = n + n に変わっています！そして両辺が同じものになったので、値として Refl を取ることができますね:

twiceIsDouble' : (n : Nat) -> n * 2 = n + n
twiceIsDouble' n =
  rewrite multDistributesOverPlusRight n 1 1 in
  rewrite multOneRightNeutral n in
  Refl

これで証明完了です:

*twiceIsDouble> :r
*twiceIsDouble> :doc twiceIsDouble
Main.twiceIsDouble : (n : Nat) -> n * fromInteger 2 = n + n
    
    
    The function is: Total & public export

このように、hole の型を x = y を使って書き換えていき、最終的に両辺を同じにして Refl で締める というのが rewrite を使った証明の基本的な流れになります。まあ最後は別に Refl じゃなくても良いんですが。

rewrite では、与えられる項の型(x = y)を調べることで、どこがどう置き換わるかが明確にわかるため、わざわざ明示的に指定する必要がないのです。ただし、登場する x は全て y に置き換えてしまうので、「登場する x のうち一部だけ y に置き換えたい」という時に使えないのは注意しましょう。

また関数ではないため、ネストする際も () をつける必要がなく、上記のように改行とインデントを工夫することで綺麗に縦にコードを続けることができます。

まとめ

replace : (x = y) -> P x -> P y は「x = y かつ P(x) ならば、 P(y) も成り立つ」という関数
- x, y, P を明示的に与える必要がある(replace {x = ...} {y = ...} {P = \z => ...})
rewrite は、hole の型の x を、 x = y を使って y に書き換えるマクロ
- rewrite (x = y 型の値) in (hole の型が書き換わったもの) という形で使う

おまけ

任意の自然数 m, n に対して m + n + m = n + m * 2 が成り立つことを証明してみてください。以下を使うとできます:

ここで証明した twiceIsDouble
plusCommutative
plusAssociative

本来は Idris2 を使うべきなのですが、型に線形性がついていて分かりづらいかなと思ったので Idris1 の方にしています。 ↩