yoshihiro503 https://blog.hatena.ne.jp/yoshihiro503/ にわとり小屋でのプログラミング https://yosh.hateblo.jp/ 自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。まず、自然数全体の型 nat を定義する。 Inductive nat : Set := | O : nat | S : nat -> nat. 次にこの自然数上での足し算を計算する plus 関数を定義する。 Fixpoint plus x y := match x with | O => y | S x => S (plus x y) end where "x + y" := (plu… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fyosh.hateblo.jp%2Fentry%2F20091023%2Fp2" title=" 自然数(エンコーディングは問わず)の加算の可換法則、結合法則、分配法則を証明。 - にわとり小屋でのプログラミング" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2009-10-23 00:00:01 rich https://yosh.hateblo.jp/entry/20091023/p2 1.0 100%