[Coq] Ring in Coq

スタート代数という勉強会に参加してきました。 そこで出された宿題のうち１問を Coq で証明してみました。まぁこの程度簡単な証明なら Coq でも出来るけど、という感じです。Coq で証明するとはどんな感じかの参考になればと思います。

Section Ring.
(* R : ring *)
Axiom R:Set.
(* plus *)
Axiom plus : R -> R -> R.
Notation "a + b" := (plus a b).
Axiom plus_assoc : forall a b c:R, (a+b)+c=a+(b+c).
Axiom plus_comm : forall a b:R, a+b=b+a.
Axiom zero : R.
Notation "0" := zero.
Axiom plus_unit_l : forall a:R, 0 + a = a.
Axiom plus_unit_r : forall a:R, a + 0 = a.
Axiom minus : R -> R.
Notation "^ a" := (minus a) (at level 90).
Axiom plus_inv_l : forall a:R, (^a) + a = 0. 
Axiom plus_inv_r : forall a:R, a + (^a) = 0. 
(* mult *)
Axiom mult : R -> R -> R.
Notation "a * b" := (mult a b).
Axiom mult_assoc : forall a b c:R, (a*b)*c=a*(b*c).
Axiom one : R.
Notation "1" := one.
Axiom mult_unit_l : forall a:R, 1 * a = a.
Axiom mult_unit_r : forall a:R, a * 1 = a.
(* commutative ring *)
Axiom mult_comm : forall a b:R, a*b = b*a.
(* distributive *)
Axiom distr_l : forall a b c:R, a*(b+c) = a*b + a*c.
Axiom distr_r : forall a b c:R, (a+b)*c = a*c + b*c.

Lemma rm_plus_l : forall a b c:R, a+b=a+c -> b=c.
Proof.
  intros a b c ab_ac.
  specialize(plus_assoc (^a) a b). intro H.
  rewrite ab_ac in H.
  rewrite <- plus_assoc in H.
  rewrite plus_inv_l in H.
  repeat rewrite plus_unit_l in H.
  assumption.
Qed.
Theorem mult_a_0 : forall a:R, a * 0 = 0.
Proof.
  intro a.
  assert(H: a*(0+0) = a*0 + 0).
    rewrite plus_unit_l. rewrite plus_unit_r. reflexivity.
  rewrite distr_l in H. 
  apply(rm_plus_l (a*0) (a*0) 0). assumption.
Qed.
End Ring.

[separation logic] jStar: Bringing separation logic to Java

jStar: Bringing separation logic to Java Java Programに対してseparation logicを使って検証するというもので、事前事後条件を与えると、ループ不変条件は自動的に計算してくれるらしい（"Loop invariants are computed automatically by means of abstract interpretation. "） 論文(PDF)：jStar: Towards Practical Verification for Java チュートリアル(PDF): How to Verify Java Program with jStar: a Tutorial