Leanで学ぼう等式推論（証明もあるよ！）
プログラムを数式のように扱う
等式を使ってプログラムを変形する
実装の高速化・導出の例
例 1) reverse → map → reverse = map（具体例は省略）
例 2) 高速な List.scanl の導出（具体例は省略）
計算量 $ O(N^2) から $ O(N) に改善
元の関数と等しいことも証明可能
性質の証明の例: scanl の性質の証明（具体例は省略）
scanl f init xs の i 番目の要素が (xs,take 1).foldl f init と等しい
等式の意味
a = b の意味
rw タクティク ができるのもライプニッツ則のおかげ では「関数が等しい」ってどういうこと？
Lean における等しさ
無視されるもの: アルゴリズム、計算量
等式推論における等しさ
プログラムが同じ値に評価される
つまり、等しい式で置き換えても、プログラムの観測可能な振る舞いが変わらないこと
副作用を分離できると嬉しい
とはいえ言語による
一方 Lean は
Lean 上の a = b のプログラムの等しさが一致していると思って良い
等式の証明も Lean が検証してくれる
Lean は最近よく話題になる
∵ 証明の信頼を「誰が言ったか」を「機械的に検証する」へ移すことができる
これ自体は良いこと
が、Lean は定義が正しいことを証明しない
形式的定義が人間の頭の中の定義と同じ意味を持つとは限らない
が、Lean は与えられた定義のものとでは厳密に議論できる
定義を人間がチェックすれば良い（リポジトリを作っておく）
が、人間も間違える
発展
コンパイラ・プログラム変換の導出