証明してみた。

Coq

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.

以下ねたばれ

続きを読む