【Coq】1+1=2の証明

8263 ワード
Coq Coq テキストリンク

coqとは

いろいろ証明したりできます。

今回は1+1=2を証明しました。
参考文献はCoq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
これに解説が丁寧に書かれていますので、なにか分からないことがあったらこの本を見ればいいと思います。
というか導入とかまともに解説しようとすると丸パクリになってしまうので、気になる方はCoq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化を買ってください。p42-p46に参考にさせていただいた記述があります。
もっと正確な内容を知りたいという方は公式のドキュメント(英語版)をみてください

コード

1+1.v
From mathcomp
  Require Import ssrnat.

Section naturalNumber.

Lemma unko_of_legends (n : nat): 1 + 1 =  2.
Proof. 
rewrite addn1.
reflexivity.
Qed.

かいせつ

自然数Coqの標準ライブラリで以下のように帰納的に定義されています。

Inductive nat : Set := O | S (n:nat).

O、S(O)、S(S(O))とかS(S(S(S(O))))とかが自然数です。
自然数の加法はssrnatの公式ドキュメントというライブラリで定義されています。
複雑でよくわからないのでssrnatの解説はパスで
1,2行目

From mathcomp
  Require Import ssrnat.

ssrnatのライブラリを読み込んでいます。これで自然数の加法の定義を読み込めました。

3,4行目

From mathcomp
  Require Import ssrnat.

Section naturalNumber.

Lemma unko_of_legends: 1 + 1 =  2.

まで読み込み、Coq IDEの上部のViewからDesplay notationsのチェックを外すとゴールエリアに

1 subgoal
______________________________________(1/1)
eq (addn (S O) (S O)) (S (S O))

と表示されます。
addn (S O) (S O)) は 1 + 1　について+を関数として書いたもので、項(term)です。

eq (addn (S O) (S O)) (S (S O)) が　1 + 1 = 2　について=の関数として書いた命題(Proposition)です。

eqは
公式のドキュメント
で一般に以下のように定義されています。　

Inductive eq (A:Type) (x:A) : A -> Prop :=
  eq_refl : eq A x x.

Propつまり命題と書かれているのがみればわかります。
自然数のequalの定義はペアノの公理とか言ってもっと混み合っているので、詳しくは公式のドキュメント
rec

細かい言葉の使い方はよくわかりませんが意味としてはだいたいこんなもんです。たぶん。