# PeanoPositive.v

まずこの前のコードに引き算のレンマを加えて、PeanoPositive.vとしてまとめた。

```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.

Require Import ZArith.
Require Import BinPos.
Definition two := myS I.
Definition ten := myS (myS (myS (myS (myS (myS (myS (myS (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.

(** (Mypplus,Pplus) and (mypmult,Pmult) are Homomorphisms *)
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.

(** Mypositive_of_positive and inversion are INJECTIVE and SURJECTIVE *)

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 myP_P_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 myP_P_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.

(** Lemmas *)
Lemma myPplus_comm : forall mp mq:mypositive,
myPplus mp mq = myPplus mq mp.
Proof.
intros mp mq.
rewrite <- myP_P_injective in |- *.
rewrite hom_myPplus_Pplus in |- *.
rewrite Pplus_comm in |- *.
rewrite <- hom_myPplus_Pplus in |- *.
rewrite myP_P_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 <- myP_P_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 myP_P_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 <- myP_P_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 myP_P_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 <- myP_P_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 myP_P_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 <- myP_P_injective in |- *.
rewrite hom_myPmult_Pmult in |- *.
rewrite Pmult_comm in |- *.
rewrite <- hom_myPmult_Pmult in |- *.
rewrite myP_P_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 <- myP_P_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 myP_P_injective in |- *; reflexivity.
Qed.

(** Ordering *)
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.

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.

(** Pcompare lemmas *)
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.

(**Pminus*)
Theorem Pminus_succ_one_l : forall p:positive,
Pminus (Psucc p) xH = p.
Proof.
intro p; induction p.
simpl in |- *.
unfold Pminus in |- *.
unfold Pminus_mask in |- *.
generalize IHp.
case p.
intro; simpl in |- *.
unfold Pminus in |- *.
unfold Pminus_mask in |- *.
intro eq; rewrite eq in |- *; reflexivity.
intro p'; unfold Psucc in |- *; unfold Pminus in |- *.
unfold Pminus_mask in |- *.
unfold Pdouble_minus_one in |- *.
intro; reflexivity.
intro; simpl in |- *; reflexivity.
simpl in |- *.
unfold Pminus in |- *.
unfold Pminus_mask in |- *.
reflexivity.
unfold Psucc in |- *; unfold Pminus in |- *.
unfold Pminus_mask in |- *.
unfold Pdouble_minus_one in |- *.
reflexivity.
Qed.

Theorem Pminus_mask_carry_succ_l : forall p q : positive,
Pminus_mask p q = Pminus_mask_carry (Psucc p) q.
Proof.
intro p; induction p; intro q; case q; simpl in |- *; try reflexivity.
intro; rewrite IHp in |- *; reflexivity.
intro; rewrite IHp in |- *; reflexivity.
case p; simpl in |- *; try reflexivity.
intro p'; induction p'; simpl in |- *; try reflexivity.
injection IHp'.
intro eq; rewrite eq in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
Qed.

Theorem Pminus_mask_carry_succ_r : forall p q : positive,
Pminus_mask_carry p q = Pminus_mask p (Psucc q).
Proof.
intro p; induction p; intro q; case q; try simpl in |- *; try reflexivity.
intro; rewrite IHp in |- *; reflexivity.
case p; try simpl in |- *; try reflexivity.
intro; rewrite IHp in |- *; reflexivity.
case p; try simpl in |- *; try reflexivity.
Qed.

Theorem Pminus_mask_succ_succ : forall p q:positive,
Pminus_mask (Psucc p)(Psucc q) = Pminus_mask p q.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
intro; rewrite IHp in |- *; reflexivity.
intro; rewrite Pminus_mask_carry_succ_l in |- *; reflexivity.
case p; simpl in |- *; try reflexivity.
intro p'; induction p'; simpl in |- *; try reflexivity.
injection IHp'; intro eq; rewrite eq in |- *; reflexivity.
intro; rewrite Pminus_mask_carry_succ_r in |- *; reflexivity.
intro; reflexivity.
case p; simpl in |- *; try reflexivity.
intro p; case p; simpl in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
reflexivity.
Qed.

Theorem Pminus_succ_succ : forall p q:positive,
Pminus (Psucc p)(Psucc q) = Pminus p q.
Proof.
intros p q; unfold Pminus in |- *; rewrite Pminus_mask_succ_succ in |- *;
reflexivity.
Qed.

(** myPminus *)
Fixpoint myPminus x y {struct y} := match x,y with
| I,_ => I
| myS x',I => x'
| myS x',myS y' => myPminus x' y'
end.

Theorem hom_myPminus_Pminus : forall x y:mypositive,
positive_of_mypositive (myPminus x y)
= Pminus (positive_of_mypositive x)(positive_of_mypositive y).
Proof.
intro x; induction x.
intro y; case y; simpl in |- *.
unfold Pminus in |- *.
unfold Pminus_mask in |- *.
reflexivity.
intro m; case (Psucc (positive_of_mypositive m)); unfold Pminus in |- *;
unfold Pminus_mask in |- *; reflexivity.
intro y; case y.
simpl in |- *.
rewrite Pminus_succ_one_l in |- *; reflexivity.
intro; simpl in |- *.
rewrite IHx in |- *.
rewrite Pminus_succ_succ in |- *; reflexivity.
Qed.
```