Coq and Lean

Coq Proof AssistantとLean Programming Language，やりたいことは基本的に同じだが，後発のLeanの方が洗練されているといえなくもない。どちらの言語も初めての人には絶対わけわからん言語だ。ちょうどChatGPTがあることだし，こういう未知の言語は生成AIに任せる。

同一のTheoremを証明する。

# Coq

実行環境はこちら。
jsCoq – The Coq Theorem Prover Online IDE

(* Import the standard library for natural numbers *)
Require Import Coq.Arith.Plus.

(* Theorem: addition is commutative for natural numbers *)
Theorem add_comm : forall a b : nat, a + b = b + a.
Proof.
  (* Use induction on a *)
  intros a b.
  induction a as [|a' IHa].
  - (* Base case: a = 0 *)
    simpl.
    rewrite Nat.add_0_r.  (* Use the fully qualified name *)
    reflexivity.
  - (* Inductive case *)
    simpl.
    rewrite IHa.
    rewrite <- Nat.add_succ_r. (* Use add_succ_r to rewrite the goal *)
    reflexivity.
Qed.

# Lean

実行環境はこちら。
Lean 4 Web

variable (R : Type*) [Ring R]

#check (add_comm : ∀ a b : R, a + b = b + a)

って，これじゃRingの出来合いの型を使ってるだけだな。どうもChatGPTの出力するコードがWeb環境で動作しない。