証明してみた。

http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。

とりあえず、問題設定

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.

Lemma A_mul_0_l: forall a, 0 * a = 0.
Proof.
  intros.
  rewrite (A_mul_comm 0 a).
  exact (A_mul_0_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.

Lemma inv_is_unique: forall a b (H: a <> 0), a * b = 1 -> A_inv a H = b.
Proof.
  intros.
  rewrite <- (A_mul_1_r (A_inv _ _)).
  rewrite <- H0.
  rewrite <- (A_mul_assoc _ _ _).
  rewrite (A_mul_comm _ a).
  rewrite (inv_is_inv a H).
  auto using A_mul_1_l.
Qed.

Lemma inv_1: forall H, A_inv 1 H = 1.
Proof.
  intros.
  apply inv_is_unique.
  auto using A_mul_1_l.
Qed.

Lemma zero_ring: 0 = 1 -> forall a, a = 0.
Proof.
  intros.
  rewrite <- (A_mul_1_r a).
  rewrite <- H.
  auto using A_mul_0_r.
Qed.

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

Lemma domain: forall a b, a * b = 0 -> a = 0 \/ b = 0.
Proof.
  intros.
  destruct (A_eq_dec b 0).
  auto.
  left.
  rewrite <- (A_mul_1_r a).
  rewrite <- (inv_is_inv b n).
  rewrite <- (A_mul_assoc _ _ _).
  rewrite H.
  auto using A_mul_0_l.
Qed.

Infix "+" := A_add.

Lemma A_add_1_r_S: forall a, a + 1 = S a.
Proof.
  intro.
  unfold A_add.
  destruct (A_eq_dec a 0).
  rewrite e. auto using S_0.
  rewrite <- S_0.
  rewrite <- (S_mul a 0 n).
  rewrite (A_mul_0_l (A_inv a _)).
  rewrite S_0.
  rewrite (A_mul_1_r a).
  auto.
Qed.

Lemma A_add_1_l_S: forall a, 1 + a = S a.
Proof.
  intro.
  unfold A_add.
  destruct (A_eq_dec 1 0).
  assert (0 = 1) by auto.
  rewrite (zero_ring H (S a)).
  auto using zero_ring.

  rewrite (inv_1 n).
  rewrite (A_mul_1_r a).
  auto using A_mul_1_l.
Qed.

Lemma A_add_dist: forall a b c,  a * (b + c) = a * b + a * c.
  intros.
  unfold A_add.
  destruct (A_eq_dec (a * b) 0).
    destruct (domain a b e).
    rewrite H.
    rewrite (A_mul_0_l _). auto using A_mul_0_l.
  destruct (A_eq_dec b 0).
    auto.
    congruence.
  destruct (A_eq_dec b 0).
    cut False. intro. contradiction.
    rewrite e in n.
    rewrite (A_mul_0_r a) in n.
    congruence.
  rewrite (A_mul_comm a c).
  rewrite (A_mul_assoc c a _).
  assert (b * (a * A_inv (a * b) n) = 1).
  rewrite <- (A_mul_assoc b a _).
  rewrite (A_mul_comm b a).
  auto using inv_is_inv.
  rewrite (inv_is_unique b _ n0 H).
  auto using A_mul_assoc.
Qed.

Lemma A_add_0_r: forall a, a + 0 = a.
Proof.
  intros.
  unfold A_add.
  destruct (A_eq_dec a 0).
  auto.
  rewrite (A_mul_0_l _).
  rewrite S_0.
  auto using A_mul_1_r.
Qed.

Lemma A_add_0_l: forall a, 0 + a = a.
Proof.
  intros.
  unfold A_add.
  destruct (A_eq_dec 0 0).
  auto.
  congruence.
Qed.

Lemma A_add_comm: forall a b, a+ b = b + a.
Proof.
  intros.
  destruct (A_eq_dec a 0) as [Ha|Ha].
  rewrite Ha.
    rewrite A_add_0_r.
    auto using A_add_0_l.
  transitivity (a * S (b * A_inv a Ha)).
  unfold A_add.
  destruct (A_eq_dec a 0).
  congruence.
  assert (A_inv a n = A_inv a Ha) by auto using inv_is_unique, inv_is_inv.
  congruence.
  rewrite <- A_add_1_r_S.
  rewrite A_add_dist.
  rewrite (A_mul_comm b).
  rewrite <- A_mul_assoc.
  rewrite inv_is_inv.
  rewrite A_mul_1_r.
  rewrite A_mul_1_l.
  auto.
Qed.

Lemma A_add_assoc_0: forall a b, (a + b) + 0 = a + (b + 0).
Proof.
   intros.
   rewrite A_add_0_r.
   rewrite A_add_0_r.
   auto.
Qed.

Lemma A_add_assoc_1: forall a b, (a + b ) + 1 = a + (b + 1).
Proof.
   intros.
   rewrite A_add_1_r_S.
   rewrite A_add_1_r_S.
   unfold A_add.
   destruct (A_eq_dec a 0).
   auto.
   auto using S_mul.
Qed.

Lemma A_add_assoc: forall a b c, (a + b) + c = a + (b + c).
Proof.
  intros.
  destruct (A_eq_dec c 0).
  rewrite e. auto using A_add_assoc_0.
  transitivity (c * (A_inv c n * a + A_inv c n * b + 1));[|rewrite A_add_assoc_1];
    repeat rewrite A_add_dist;
    repeat rewrite <- (A_mul_assoc c _ _);
    repeat rewrite inv_is_inv;
    repeat rewrite A_mul_1_l;
    rewrite A_mul_1_r; auto.
Qed.

Lemma A_neg_ex: forall a, { a': A | a + a' = 0 }.
Proof.
  intros.
  rewrite <- (A_mul_1_r a).
  exists (a * S_inv 0).
  rewrite <- A_add_dist.
  rewrite A_add_1_l_S.
  rewrite S_inv_r.
  auto using A_mul_0_r.
Qed.