Coq 交互式证明乘法幺元交换律

　　先定义三条公理（其实公理 2 对于这里证明幺元交换律不重要）：

　　$ forall a, b in N $，$ e $ 是单位元，满足下面三条运算法则：

　　1. $ a b = b a $（交换律）.

　　2. $ (a b) c = a (b c) $（结合律）.

　　3. $ e a = a $（幺元）.

　　根据公理，我们有如下假设：

　　$ a e = a $.

　　现在使用 coq 来证明我们的假设：

Axiom mult_ring1 : forall a b:nat,
  a * b = b * a.
Axiom mult_ring2 : forall a b c:nat,
  (a * b) * c = a * (b * c).
Axiom mult_ring3 : forall a e:nat,
  e * a = a.

Theorem unit_commutative_law : forall a e:nat, a * e = a.
Proof.
  intros a e.
  rewrite -> mult_ring1.
  rewrite -> mult_ring3.
  reflexivity.
Qed.
Print unit_commutative_law.

　　也就是我们先对假设条件使用公理 1 进行重写，然后得到 $ a e = e a $，然后再根据公理3，就可以写为 $ a e = e a = a $，再根据自反性 $ a = a $，于是我们的定理得到证明。

　　感觉挺不错的，对于证明逻辑有一些帮助。