読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676

まずは集合AとA上の掛け算とサクセッサSを仮定。この部分はid:kikxさんのコードのコピー。

Axiom A : Set.
Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }.

Axiom A_mul : A -> A -> A.
Axiom A_zero: A.
Axiom A_one: A.

Infix "*" := A_mul.
Notation "0" := A_zero.
Notation "1" := A_one.

Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c).
Axiom A_mul_comm: forall a b, a * b = b * a.
Axiom A_mul_1_r: forall a, a * 1 = a.
Axiom A_mul_inv_ex: forall a, a <> 0 -> { a': A | a * a' = 1 }.
Axiom A_mul_0_r: forall a, a * 0 = 0.

Lemma A_mul_1_l: forall a, 1 * a = a.
Proof.
  intros.
  rewrite (A_mul_comm 1 a).
  exact (A_mul_1_r a).
Qed.

Definition A_inv a (H: a <> 0) :=
  let (a', H) := A_mul_inv_ex a H in a'.

Axiom S: A -> A.
Axiom S_inv: A -> A.

Axiom S_inv_l: forall a, S_inv (S a) = a.
Axiom S_inv_r: forall a, S (S_inv a) = a.
Axiom S_0:  S 0 = 1.
Axiom  S_mul: forall a b (H: a <> 0),
  S (a * S (b * A_inv a H)) = a * S (S b * A_inv a H).

Lemma inv_is_inv: forall a (H: a <> 0), a * A_inv a H = 1.
Proof.
  intros.
  unfold A_inv.
  case (A_mul_inv_ex a H).
  trivial.
Qed.

ここからA上の足し算も仮定。同時に足し算が満たすべき公理も仮定。

Parameter A_add : A -> A -> A.
Infix "+" := A_add.
Hypothesis A_add_1_r_S: forall a, a + 1 = S a.
Hypothesis A_add_dist: forall a b c,  a * (b + c) = a * b + a * c.
Hypothesis A_add_0_r: forall a, a + 0 = a.
Hypothesis A_add_comm: forall a b, a+ b = b + a.
Hypothesis A_add_assoc: forall a b c, (a + b) + c = a + (b + c).
Hypothesis A_neg_ex: forall a, { a': A | a + a' = 0 }.

id:kikxさんの定義した足し算をA_kikxs_addという名前で用意し、上で仮定した抽象的な足し算A_addがA_kikxs_addと必ず等価になることを証明した。このことからA_addは一意であることが示せた。

Definition A_kikxs_add a b :=
  match A_eq_dec a 0 with
  | left _ => b
  | right H => a * S (b* A_inv a H)
  end.

Theorem uniqueness : forall a b, A_add a b = A_kikxs_add a b.
Proof.
 intros a b.
 unfold A_kikxs_add.
 case (A_eq_dec a 0).

  intro eq; rewrite eq.
  rewrite A_add_comm.
  rewrite A_add_0_r.
  reflexivity.

  intro neq.
  pattern a at 1; rewrite <- (A_mul_1_r a).
  pattern b at 1; rewrite <- (A_mul_1_l b).
  pattern 1 at 2; rewrite <- (inv_is_inv a neq).
  rewrite (A_mul_assoc).
  rewrite <- A_add_dist.
  rewrite (A_add_comm 1 _).
  rewrite A_add_1_r_S.
  rewrite (A_mul_comm _ b).
  reflexivity.
Qed.