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

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.