Coq Proof Assistant

Coqというのは定理証明支援系。数学の証明を形式的にチェックしてくれるツールだ。
数学書を漫然と眺めていても仕方ないので，Coqのコードに書きなおしながら読めばいいんじゃないか，と思いついた。

「演習　群・環・体　入門」は，本来整数の代数的定義がこの前にあって，「この公理系だけから証明しようね」という流れなのだが，今回は既存Libraryで端折ってしまった。
「はじめての数理論理学」は著者がCoqの授業もやってらっしゃるのか，非常に読みやすい，んだけど私がCoqに不慣れなせいできれいに証明が書けてない。

こういう証明をいきなり書き下すのは，以前ならとんでもない苦労が必要だった。
今はChatGPTがある。ChatGPTにCoqのコード書いてください，とお願いすれば，それなりのコードが出来てくるのだ。

JavaやPythonなどよりも，Coqのような高難易度でシェアの少ない言語の方が，ChatGPTの恩恵を受けられる。ChatGPTはマイナーな言語の先生替わりになってくれる。
そもそもJavaやPythonは，今後まともにコーディングスキルが必要になるか分からない。
雑多な業務のためのコードは，「雑多な業務」の方を何とかしないかぎりゴミの山なのだ。
生成AIにまるっと投げてしまった方がいい，という意見が出てきてもおかしくない。

それよりも，数学の，特に定義をどう作るか，などの「やる人の数は少ないが，後々の効果は絶大」な分野の方が時間をかける価値がある気がする。

理屈はともかく，数学書をCoqで写経するのは楽しい。

(* 新妻弘，「演習　群・環・体　入門」，共立出版株式会社 より *)
Require Import ZArith.
Open Scope Z_scope.

Theorem thm_1_1 : forall a b c : Z , a + b = a + c -> b = c.
Proof.
  intros a b c H.
  apply Z.add_cancel_l with (p := a).
  assumption.
Qed.

Theorem thm_1_2_1 : forall a : Z , 0 * a = 0.
Proof.
  intros a.
  auto.
Qed.

Theorem thm1_2_2 : forall a : Z , a * 0 = 0.
Proof.
  intros.
  rewrite Z.mul_0_r.
  reflexivity.
Qed.

Theorem thm1_2_3 : forall a : Z , a * 0 = 0 * a.
Proof.
  simpl.
  intro a.
  apply thm1_2_2.
Qed.

Theorem thm1_3_1 : forall a : Z , - ( - a ) = a.
Proof.
  intros.
   rewrite <- Z.opp_involutive.
   reflexivity.
Qed.


(* 山田俊行，「はじめての数理論理学」，森北出版 より *)
Theorem thm_p_61 :
forall P Q R S : Prop, (P /\ Q) /\ (P -> R /\ S) -> S.
Proof.
  intros.
  destruct H.
  destruct H.
  destruct H0 as [H2].
  exact H.
  exact H0.
Qed.