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.