「Coqで証明書いてみた」の１行づつの実行を記録してみた。

19710 ワード
Coq coqide Coq テキストリンク

動作環境

CoqIDE 8.7.1
mac OS 10.13.3 High Sierra

Coqで証明書いてみた

の１行づつの実行を記録してみた。
将来説明を追記。

Require Import Arith.

Theorem Th1 : 
forall (n : nat),
(exists m : nat, n = m * 2)
-> exists k : nat,  n * 2 = k * 4.

Proof.
intros.
destruct H.
exists x.
rewrite H.
rewrite mult_assoc_reverse.
simpl.
reflexivity.
Qed.

Require Import Arith.

"Forward One Command"すると"Messages"に下記表示あり。

[Loading ML file z_syntax_plugin.cmxs ... done]

[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]

Theorem Th1 : 
forall (n : nat),
(exists m : nat, n = m * 2)
-> exists k : nat,  n * 2 = k * 4.

"Forward One Command"すると右上窓に下記表示。

1 subgoal
______________________________________(1/1)
forall n : nat,
(exists m : nat, n = m * 2) -> exists k : nat, n * 2 = k * 4

Proof.
intros.

「証明」「出だし」
"Forward One Command"２回すると右上窓に下記表示。

1 subgoal
n : nat
H : exists m : nat, n = m * 2
______________________________________(1/1)
exists k : nat, n * 2 = k * 4

destruct H.

「自爆」
"Forward One Command"すると右上窓に下記表示。

1 subgoal
n, x : nat
H : n = x * 2
______________________________________(1/1)
exists k : nat, n * 2 = k * 4

exists x.

「存在」
"Forward One Command"すると右上窓に下記表示。

1 subgoal
n, x : nat
H : n = x * 2
______________________________________(1/1)
n * 2 = x * 4

rewrite H.

「書き換え」
"Forward One Command"すると右上窓に下記表示。

1 subgoal
n, x : nat
H : n = x * 2
______________________________________(1/1)
x * 2 * 2 = x * 4

rewrite mult_assoc_reverse.

「書き換え」
"Forward One Command"すると右上窓に下記表示。

1 subgoal
n, x : nat
H : n = x * 2
______________________________________(1/1)
x * (2 * 2) = x * 4

simpl.

「単純」
"Forward One Command"すると右上窓に下記表示。

1 subgoal
n, x : nat
H : n = x * 2
______________________________________(1/1)
x * 4 = x * 4

reflexivity.

「反射性」
"Forward One Command"すると右上窓に下記表示。

No more subgoals.

Qed.

「証明終わり」
"Forward One Command"すると右上窓に下記表示。

Th1 is defined