掛け算から足し算を作る(足し算の一意性について)
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.