ポジティブ型とマイポジティブ型

（＊＊ Remark
今回はZArithモジュールを使うよ。
Require Import ZArith.
をタイプしてね。
＊）

導入

Coqでは、整数全体の型はZで表され、次のように定義されている。

Coq < Print Z.
Inductive Z : Set :=
   Z0 : Z
 | Zpos : positive -> Z
 | Zneg : positive -> Z

Z0はゼロで、Zposは正の数、Znegは負の数を表している。
ここでpositiveという型が使われているが、これは１以上の整数全体を表している。
Coqでは、このpositive型に工夫がしてあって、現実のプログラムとの親和性をよくしている。
具体的には次のような再帰的な定義になっている。

Coq < Print positive.
Inductive positive : Set :=
   xI : positive -> positive
 | xO : positive -> positive
 | xH : positive

これは一見なんのことやらわかりにくいが、二進数による正の整数を表現している。
xIは１、xOは０、そしてxHは最高桁の１を表している。

1100は、xO (xO (xI xH))とあらわされ、
1は、xHとあらわされ、
10110は、xO (xI (xI (xO xH)))とあらわされる。

右側が大きい位の桁となることと、正の整数なので必ず最高桁が1になることに注意しよう。
このような実装によって、Zの演算や大小比較などの実行効率をよくしている。
しかし、この表現だと、理論的な性質を証明することがちょっとめんどくさくなるように感じた。
Coqの標準ライブラリには、基本的な性質がほとんどそろっており、succを使った普通の数学的帰納法もちゃんと使えるようになっているが、やっぱり、自分で何か考えたりするときにめんどくさくなるような気がした。

ということで、既存のpositive型に対してマイポジティブ型を考えてみた。

結論

今回はそのマイポジティブ型上での足し算とかけ算と大小比較（順序）を構成し、次の性質を証明した。

• マイポジティブ型が足し算に関して可換半群となること
  • 足し算における結合法則
  • 足し算における交換法則

• マイポジティブ型がかけ算に関して可換モノイドとなること
  • かけ算における単位元の存在
  • かけ算における結合法則
  • かけ算における交換法則

• その他の演算法則
  • 左分配法則
  • 右分配法則

• マイポジティブ型がマイ小なりイコール関数に関して順序集合となること
  • マイ小なりイコール関数の反射律
  • マイ小なりイコール関数の反対称律
  • マイ小なりイコール関数の推移律

• ポジティブ型といろんな意味で同型になること
  • マイポジティブ型はポジティブ型と集合として同型になる。
  • 足し算に関してポジティブ型の構造を保存する。（半群同型）
  • かけ算に関してポジティブ型の構造を保存する。（モノイド同型）
  • 大小比較に関してポジティブ型の構造を保存する。（順序同型）

詳細

まず、マイポジティブ型の定義。自然数のnat型をまねした。Iは１を意味する。

Inductive mypositive : Set :=
 | I : mypositive
 | myS : mypositive -> mypositive.

次に早速足し算とかけ算を定義する。ポジティブ型に比べて定義がすっきりしている。

Fixpoint mypplus mp1 mp2 {struct mp1} := match mp1 with
  | I => myS mp2
  | myS mp1' => myS (mypplus mp1' mp2)
  end.
Fixpoint mypmult mp1 mp2 {struct mp1} := match mp1 with
  | I => mp2
  | myS mp1' => mypplus mp2 (mypmult mp1' mp2)
  end.

次にポジティブ型といろんな構造の保存を証明するための同型写像を次の関数で具体的に定義した。

Definition two := myS I.  (*これは２*)
Fixpoint mypositive_of_positive p := match p with
  | xH => I
  | xO p' => mypmult two (mypositive_of_positive p')
  | xI p' => myS (mypmult two (mypositive_of_positive p'))
  end.
Fixpoint positive_of_mypositive mp := match mp with
  | I => xH
  | myS mp' => Psucc (positive_of_mypositive mp')
  end.

足し算に関して準同型になっていることの証明

Theorem hom_mypplus_Pplus : forall mp1 mp2:mypositive,
  positive_of_mypositive (mypplus mp1 mp2)
  = Pplus (positive_of_mypositive mp1) (positive_of_mypositive mp2).
Proof.
intros mp1 mp2; induction mp1.
 unfold mypplus in |- *.
   unfold positive_of_mypositive in |- *; fold positive_of_mypositive in |- *.
   apply Pplus_one_succ_l.
simpl in |- *.
  rewrite IHmp1 in |- *.
  rewrite Pplus_succ_permute_l in |- *.
  reflexivity.
Qed.

かけ算に関して準同型になっていることの証明

Lemma Pmult_succ_l : forall p q:positive,
 Pmult (Psucc p) q = Pplus q (Pmult p q).
Proof.
intros p q; rewrite Pplus_one_succ_l in |- *.
rewrite Pmult_plus_distr_r in |- *.
simpl in |- *; reflexivity.
Qed.

Theorem hom_mypmult_Pmult : forall mp1 mp2:mypositive,
  positive_of_mypositive (mypmult mp1 mp2)
  = Pmult (positive_of_mypositive mp1) (positive_of_mypositive mp2).
Proof.
intros mp1 mp2; induction mp1.
 simpl in |- *; reflexivity.
simpl in |- *.
  rewrite hom_mypplus_Pplus in |- *.
  rewrite IHmp1 in |- *.
  rewrite Pmult_succ_l in |- *.
  reflexivity.
Qed.

集合として同型であることを示すために逆写像が存在することを証明。
つまり
φ:= positive_of_mypositive
ψ:= mypositive_of_positive
としたときに φoψ = id かつ ψoφ = id となることを証明した。

Lemma mypplus_succ_permute_r : forall myp myq:mypositive,
  mypplus myp (myS myq) = myS (mypplus myp myq).
Proof.
intro myp; induction myp.
 intro; simpl in |- *.
   reflexivity.
intro myq; simpl in |- *.
  rewrite IHmyp in |- *; reflexivity.
Qed.

Lemma succ_hom : forall p:positive, 
 mypositive_of_positive (Psucc p) = myS (mypositive_of_positive p).
Proof.
intro p; induction p.
 simpl in |- *.
   rewrite IHp in |- *.
   simpl in |- *.
   rewrite mypplus_succ_permute_r in |- *.
   reflexivity.
simpl in |- *.
  reflexivity.
simpl in |- *.
  reflexivity.
Qed.

Theorem p_myp_injective : forall mp:mypositive,
 mypositive_of_positive (positive_of_mypositive mp) = mp.
Proof.
intro mp; induction mp.
 simpl in |- *; reflexivity.
simpl in |- *.
  rewrite succ_hom in |- *.
  rewrite IHmp in |- *; reflexivity.
Qed.

Theorem p_myp_surjective : forall p:positive,
 positive_of_mypositive (mypositive_of_positive p) = p.
Proof.
intro p; induction p.
 simpl in |- *.
   rewrite hom_mypplus_Pplus in |- *.
   rewrite IHp in |- *.
   rewrite xI_succ_xO in |- *; rewrite <- Pplus_diag in |- *.
   reflexivity.
simpl in |- *.
  rewrite hom_mypplus_Pplus in |- *.
  rewrite IHp in |- *.
  rewrite Pplus_diag in |- *; reflexivity.
simpl in |- *; reflexivity.
Qed.

足し算に関する交換法則

Lemma mypplus_comm : forall mp mq:mypositive,
  mypplus mp mq = mypplus mq mp.
Proof.
intros mp mq.
rewrite <- injective in |- *.
rewrite hom_mypplus_Pplus in |- *.
rewrite Pplus_comm in |- *.
rewrite <- hom_mypplus_Pplus in |- *.
rewrite injective in |- *; reflexivity.
Qed.

足し算に関する結合法則

Lemma mypplus_assoc: forall mp mq mr : mypositive,
 mypplus mp (mypplus mq mr) = mypplus (mypplus mp mq) mr.
Proof.
intros mp mq mr.
rewrite <- injective in |- *.
rewrite hom_mypplus_Pplus in |- *.
rewrite hom_mypplus_Pplus in |- *.
rewrite <- Pplus_assoc in |- *.
rewrite <- hom_mypplus_Pplus in |- *.
rewrite <- hom_mypplus_Pplus in |- *.
rewrite injective in |- *; reflexivity.
Qed.

左分配法則

Lemma mypmult_plus_distr_l: forall mp mq mr : mypositive,
 mypmult mp (mypplus mq mr) = mypplus (mypmult mp mq) (mypmult mp mr).
Proof.
intros mp mq mr; rewrite <- injective in |- *.
rewrite hom_mypplus_Pplus in |- *; rewrite hom_mypmult_Pmult in |- *;
 rewrite hom_mypmult_Pmult in |- *.
rewrite <- Pmult_plus_distr_l in |- *.
rewrite <- hom_mypplus_Pplus in |- *; rewrite <- hom_mypmult_Pmult in |- *.
rewrite injective in |- *; reflexivity.
Qed.

右分配法則

Lemma mypmult_plus_distr_r: forall mp mq mr : mypositive, 
 mypmult (mypplus mp mq) mr = mypplus (mypmult mp mr) (mypmult mq mr).
Proof.
intros mp mq mr; rewrite <- injective in |- *.
rewrite hom_mypplus_Pplus in |- *; rewrite hom_mypmult_Pmult in |- *;
 rewrite hom_mypmult_Pmult in |- *.
rewrite <- Pmult_plus_distr_r in |- *.
rewrite <- hom_mypplus_Pplus in |- *; rewrite <- hom_mypmult_Pmult in |- *.
rewrite injective in |- *; reflexivity.
Qed.

かけ算における単位元の存在

Lemma mypmult_1_r: forall mp : mypositive, mypmult mp I = mp.
Proof.
intro mp; induction mp.
 simpl in |- *; reflexivity.
 simpl in |- *; rewrite IHmp in |- *; reflexivity.
Qed.

かけ算に関する交換法則

Lemma mypmult_comm: forall mp mq : mypositive,
 mypmult mp mq = mypmult mq mp.
Proof.
intros mp mq.
rewrite <- injective in |- *.
rewrite hom_mypmult_Pmult in |- *.
rewrite Pmult_comm in |- *.
rewrite <- hom_mypmult_Pmult in |- *.
rewrite injective in |- *; reflexivity.
Qed.

かけ算に関する結合法則

Lemma mypmult_assoc: forall mp mq mr : mypositive, 
 mypmult mp (mypmult mq mr) = mypmult (mypmult mp mq) mr.
Proof.
intros mp mq mr.
rewrite <- injective in |- *.
rewrite hom_mypmult_Pmult in |- *.
rewrite hom_mypmult_Pmult in |- *.
rewrite <- Pmult_assoc in |- *.
rewrite <- hom_mypmult_Pmult in |- *.
rewrite <- hom_mypmult_Pmult in |- *.
rewrite injective in |- *; reflexivity.
Qed.

大小比較のためのコンペア関数を定義した

Fixpoint Mypcompare x y {struct y} : comparison :=
 match x,y with
 | I,I => Eq
 | myS _, I => Gt
 | I, myS _ => Lt
 | myS x', myS y' => Mypcompare x' y'
 end.

Definition Myp_lt x y := Mypcompare x y = Lt.

マイ小なりイコール関数

Definition Myp_le x y := x=y ?/ Myp_lt x y.

コンペア関数に関する諸性質

Theorem MypEq_eq : forall x y:mypositive,
  Mypcompare x y = Eq -> x = y.
Proof.
intro x; induction x; intro y; induction y.
 intro; reflexivity.
unfold Mypcompare in |- *; intro eq;  discriminate eq.
unfold Mypcompare in |- *; intro eq;  discriminate eq.
simpl in |- *; intro H; rewrite (IHx y H) in |- *; reflexivity.
Qed.

Lemma ord4 : forall x y:mypositive,
 Myp_lt x y -> not (Myp_lt y x).
Proof.
intro x; induction x; intro y; induction y.
 intro lt; unfold Myp_lt in lt.
   unfold Mypcompare in lt.
    discriminate lt.
intro; intro lt.
  unfold Myp_lt in lt.
  unfold Mypcompare in lt.
   discriminate lt.
intro lt; unfold Myp_lt in lt; unfold Mypcompare in lt;  discriminate lt.
unfold Myp_lt in |- *; simpl in |- *.
  unfold Myp_lt in IHx.
  apply IHx.
Qed.

Lemma ord5 : forall x y z:mypositive,
 Myp_lt x y /? Myp_lt y z -> Myp_lt x z.
Proof.
intro x; induction x; intro y; induction y; intro z; induction z.
 intro H; elim H; intros H1 H2.
   unfold Myp_lt in H1; unfold Mypcompare in H1;  discriminate H1.
intro H; elim H; intro H1; unfold Myp_lt in H1; unfold Mypcompare in H1;
  discriminate H1.
intro H; elim H; intros H1 H2.
  elim (ord4 I (myS y) H1).
  apply H2.
intro; unfold Myp_lt in |- *; unfold Mypcompare in |- *; reflexivity.
intro H; elim H; intros H1 H2; unfold Myp_lt in H2; unfold Mypcompare in H2;
  discriminate H2.
intro H; elim H; intro H1; unfold Myp_lt in H1; unfold Mypcompare in H1;
  discriminate H1.
intro H; elim H; intros H1 H2; unfold Myp_lt in H2; unfold Mypcompare in H2;
  discriminate H2.
unfold Myp_lt in |- *; simpl in |- *.
  unfold Myp_lt in IHx; apply IHx.
Qed.

マイ小なりイコール関数によってマイポジティブ集合が順序集合となることを証明する。さっき証明したコンペア関数の諸性質を使えばいずれも簡単に証明できるが、そこの部分は別のorderedsetというモジュールによって、少し一般的な性質を証明した。本質ではないのでここでは省略するが、そのモジュールを使えば順序集合であることは簡単に証明できる。

Require Import orderedset.
(**反射律*)
Lemma ord1 : forall x:mypositive, Myp_le x x.
Proof.
apply (t1 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.
(**反対称律*)
Lemma ord2 : forall x y:mypositive,
 Myp_le x y /? Myp_le y x -> x = y.
Proof.
apply (t2 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.
(**推移律*)
Lemma ord3 : forall x y z:mypositive,
 Myp_le x y /? Myp_le y z -> Myp_le x z.
Proof.
 apply (t3 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.

次に、先ほどのφ:= positive_of_mypositive を使って、順序同型になることの証明をするが、以外に大変だった。なぜなら、既存のポジティブ型上での順序に関する基本的な性質が標準ライブラリから、あまり見つけられなかったからだ。
まずは準備として、既存のポジティブコンペア関数に関する諸性質を証明した。

Lemma Pcompare_lt_xH_lt : forall p:positive,
 Pcompare xH p Lt = Lt.
Proof.
intro p; case p; simpl in |- *; trivial.
Qed.

Lemma Pcompare_gt_lt_succ : forall p q:positive,
 Pcompare p q Gt = Pcompare (Psucc p) q Lt.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
 apply IHp.
apply IHp.
reflexivity.
intro mm; reflexivity.
intro mm; reflexivity.
reflexivity.
intro p; rewrite Pcompare_lt_xH_lt in |- *; reflexivity.
intro p; rewrite Pcompare_lt_xH_lt in |- *; reflexivity.
reflexivity.
Qed.

Lemma Pcompare_lt_gt_succ : forall p q:positive,
 Pcompare p q Lt = Pcompare p (Psucc q) Gt.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
 apply IHp.
intro mm; reflexivity.
case p; simpl in |- *; trivial.
apply IHp.
intro mm; reflexivity.
case p; trivial.
intro mm; reflexivity.
intro mm; reflexivity.
reflexivity.
Qed.

Theorem Pcompare_succ : forall (p q:positive) (C:comparison),
  Pcompare (Psucc p)(Psucc q) C = Pcompare p q C.
Proof.
intro p; induction p; intros q C; case q; simpl in |- *.
 intro q'; apply IHp.
intro q'; rewrite Pcompare_gt_lt_succ in |- *; reflexivity.
case p; simpl in |- *; trivial.
intro q'; rewrite Pcompare_lt_gt_succ in |- *; reflexivity.
intro mm; reflexivity.
case p; trivial.
intro p; case p; trivial.
intro p; case p; trivial.
reflexivity.
Qed.

最後に順序同型であることを証明した。

(** 順序同型 *)
Theorem hom_ord_mypcompare_pcompare : forall x y:mypositive,
  Mypcompare x y
   = Pcompare (positive_of_mypositive x) (positive_of_mypositive y) Eq.
Proof.
intro x; induction x; intro y; case y; simpl in |- *.
 reflexivity.
intro m; case (positive_of_mypositive m); simpl in |- *; trivial.
case (positive_of_mypositive x); trivial.
intro y'; rewrite Pcompare_succ in |- *.
  apply IHx.
Qed.
<|