-数学- Lean4のお勉強　証明支援、rw, applyタクティク

これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。

使用するテキストはMathematics In Lean(通称MIL)にしました。

Mathematics in Lean — Mathematics in Lean 0.1 documentation

もう１つ、"Theorem Proving In Lean4"(通称TPIL)というテキストもありそちらは有志の皆様による日本語版もあります。両者の最大の違いは、MILはmathlib4という証明ライブラリも利用して初等的な数学の証明をLean4でどうやるか説明しているのに対して、TPILの方はLean4の定理証明支援の背景理論とそれに基づく概念をきちんと説明してくれるようです。TPILを見るといきなり型理論と依存型から入っていくのですが、MILの方はタクティクを使った証明の練習のような感じです。私の興味が普通の数学の証明をLean4でどうやるか、なのでMILから取り組むことにしました。

MILの目次は次のとおりです。

基本

論理

集合と関数

初等整数論

構造

階層

群と環

位相

微分計算

積分と測度論

まずは初等整数論くらいまでは真面目にやってそのあとは面白そうなところをつまみ食いできそうならしていきたいと思っています。

今回は基本のところでrewriteタクティクの勉強です。このタクティクは等式を用いてゴールや仮定を変形していきます。この両辺が等しくなったら証明終了です。使える等式はその分野の公理や既に証明済みの等式です。

基本ではものすごく基本的なことをやります。以前に記事にしたNatural Number Gameのやり方でどんどん証明が進みます。１つだけ紹介します。

乗算*と加算+を持つ環で2*a=a+aを証明する。前提とするのは次の３つ：

add_mul: (a+b)*c=a*c+b*c（環の分配則公理）

one_mul: 1*a=a（環の乗算の単位元公理）

one_add_one_eq_two: 1+1=2（元の加算定理）

以下の２行が形式化された2*a=a+a定理とその証明：

theorem two_mul (a : R) : 2 * a = a + a := by

rw [← one_add_one_eq_two, add_mul, one_mul]

２行目の証明の解説は次のとおり：

証明のゴールを前提を使って変形していくことがrwタクティク。

2*a = a+a に1+1=2を右から左に適用すると

(1+1)*a=a+a 、にadd_mulを左から右に適用すると

1*a+1*a=a+a 、にone_mulを左から右に適用すると

a+a=a+a、両辺が等しくなったので証明終了。