自然数とリスト: 自動証明 (3.3)

Coqさんは非常に賢いので、実は、今回くらいの証明は自動でやってくれます。

Proof.
 intros.
 omega.
Qed.

omega はプレスバーガー算術という美味しそうな名前の理論の簡易全自動ソルバーで、整数に関する等式や不等式のかなりの部分を自動的に証明してくれます。

omega

整数/自然数の、足し算引き算や定数倍に関する、等式や不等式を自動証明。変数と変数の掛け算があると使えない。

ring

足し算引き算掛け算に関する等式を、単に式を整理することで自動証明。不等式は使えない。

field

足し算引き算掛け算割り算に関する等式を、単に式を整理することで自動証明。不等式は使えない。

fourier

実数に関する線形不等式の自動証明

これらがないと、数式の証明はひたすらSearchAboutとrewriteを繰り返す退屈な作業になってしまうことが多いので、覚えておかないと大変です。数式の証明で困ったらomega! この入門記事シリーズでも、今後はomega/ring/fieldで証明できるところは使っていきます。