「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

自己参照

「coq入門」の入門

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

coq(ide)を使おう　または　初めてのcop(ide) mac編

Godel’s Incompleteness Theorem in coq 壁いくつ、今壁4つ

「Coqの余帰納法でハマってしまった」を記録

MacintoshでCoqide

文書履歴(document history)

ver. 0.01 初稿 20180318
ver. 0.04 URL追記　20230226

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.