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.