[Coq] Sample of Setoid

先日のFormal Methods Forumで話したsetoidの話のCoqのコード。

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Arith.
Require Import Compare_dec.
Require Import Omega.

Section MyZ.

(* 整数 Z' を構成するのに、nat * nat に同値関係 Z'eq を入れたものを用いる。
  (a,b) in nat*nat に対し、a-b でZ'を作る、と考えてよい。 *)

(* Z' のコンストラクタ *)
Inductive Z' : Set :=
| mkZ' : nat -> nat -> Z'.

(* 同値関係 : (a,b) =Z= (c,d) iff a+d = b+c *)
Definition Z'eq (z z':Z') : Prop :=
  let (a,b) := z in
  let (c,d) := z' in
  a + d = b + c.

Notation "a =Z= b" := (Z'eq a b) (at level 70).

(* 後々の証明で使いやすい補題 *)
Lemma Z'eq_inv : forall a b c d, (mkZ' a b) =Z= (mkZ' c d) ->
  {exists q, (a=c+q /\ b=d+q)} + {exists q, (a+q=c /\ b+q=d)}.
Proof.
  intros.  simpl in H.
  destruct (le_lt_dec a c).
    (* a <= c *)
    right.  exists (c - a).  omega.
    (* c < a *)
    left.  exists (a - c).  omega.
Qed.

(* Z'eq が同値関係であることを証明する *)
Print reflexive.
Lemma Z'eq_refl : reflexive Z' Z'eq.
Proof.
  unfold reflexive.  intros.  destruct x.
  unfold Z'eq.  omega.
Qed.

Print symmetric.
Lemma Z'eq_sym : symmetric Z' Z'eq.
Proof.
  unfold symmetric.  intros.  destruct x.  destruct y.
  unfold Z'eq in *.  omega.
Qed.

Print transitive.
Lemma Z'eq_trans : transitive Z' Z'eq.
Proof.
  unfold transitive.  intros.  destruct x. destruct y. destruct z.
  unfold Z'eq in *.  omega.
Qed.

(* Z'eq が同値関係であることが示せたので Setoid を構成する *)
Add Parametric Relation : Z' Z'eq
  reflexivity proved by Z'eq_refl
  symmetry proved by Z'eq_sym
  transitivity proved by Z'eq_trans
  as Z'_rel.

(* Z' 上の演算を定義する *)
Definition Z'plus (z z':Z') : Z' :=
  let (a,b) := z in
  let (c,d) := z' in
  mkZ' (a+c) (b+d).

Add Parametric Morphism : Z'plus with
  signature Z'eq ==> Z'eq ==> Z'eq as Z'_plus_mor.
Proof.
  (* Goal := x =Z= y -> x0 =Z= y0 -> Z'plus x x0 =Z= Z'plus y y0
  Z'plus が well-defined であることを示す必要がある *)
  intros.  destruct x; destruct y; destruct x0; destruct y0.
  unfold Z'eq in *.  unfold Z'plus.  omega.
Qed.

(* 準備 *)
Lemma Z'eq_plus_id_l : forall z a, Z'plus (mkZ' a a) z =Z= z.
Proof.
  intros.  destruct z.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

Lemma Z'eq_plus_comm : forall z z', Z'plus z z' =Z= Z'plus z' z.
Proof.
  intros.  destruct z; destruct z'.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

(* setoid_rewrite を使ってみる例 *)
Lemma Z'eq_plus_id_r : forall z a, Z'plus z (mkZ' a a) =Z= z. 
Proof.
  intros.
  setoid_rewrite (Z'eq_plus_comm z (mkZ' a a)).
  apply Z'eq_plus_id_l.
Qed.

End MyZ.