Idris の replace と rewrite

## はじめに

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

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

## 前提

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

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

## どんな話？

`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` の定義](https://github.com/idris-lang/Idris-dev/blob/80fa67e719d9ae69cec01ca94cb0183268d0eb72/libs/prelude/Prelude/Nat.idr#L61-L66)は以下となっています:

```idr
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` があります。この関数の型を簡略化して書くと、

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

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

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

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

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

となります。

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

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

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

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

```idr
multOneRightNeutral n: n * 1 = n
```

となりますね。

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

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

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

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

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

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

となります。ここまでで

```idr
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 な引数なので、`{}` を使って指定する必要があります:

```idr
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
```

以上、まとめると:

```idr
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に則って、型から始めます:

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

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

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

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

```idr
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` があったので、これを利用して、

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

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

```idr
*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` がありました:

```idr
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 の型を見てみましょう:

```idr
*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` を取ることができますね:

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

これで証明完了です:

```idr
*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`