PeanoZArith.v
次に、このPeanoPositiveを使って、PeanoZという整数型を作った。
Require Import PeanoPositive. Inductive Z : Set := | Z0 : Z | Zpos : mypositive -> Z | Zneg : mypositive -> Z. Definition Zplus x y := match x,y with | Z0, y => y | x, Z0 => x | Zpos p, Zpos q => Zpos (myPplus p q) | Zpos p, Zneg q => match myPcompare p q with | Eq => Z0 | Lt => Zneg (myPminus q p) | Gt => Zpos (myPminus p q) end | Zneg p, Zpos q => match myPcompare p q with | Eq => Z0 | Lt => Zpos (myPminus q p) | Gt => Zneg (myPminus p q) end | Zneg p, Zneg q => Zneg (myPplus p q) end. Definition Zmult x y := match x,y with | Z0, _ => Z0 | _, Z0 => Z0 | Zpos p, Zpos q => Zpos (myPmult p q) | Zpos p, Zneg q => Zneg (myPmult p q) | Zneg p, Zpos q => Zneg (myPmult p q) | Zneg p, Zneg q => Zpos (myPmult p q) end. (** myz -> z *) Definition PeanoZ_of_Z z := match z with | ZArith.BinInt.Z0 => Z0 | ZArith.BinInt.Zpos p => Zpos (mypositive_of_positive p) | ZArith.BinInt.Zneg p => Zneg (mypositive_of_positive p) end. Definition Z_of_PeanoZ x := match x with | Z0 => ZArith.BinInt.Z0 | Zpos p => ZArith.BinInt.Zpos (positive_of_mypositive p) | Zneg p => ZArith.BinInt.Zneg (positive_of_mypositive p) end. Lemma hom_PZplus_Zplus_posneg : forall p q:mypositive, Z_of_PeanoZ (Zplus (Zpos p) (Zneg q)) = ZArith.BinInt.Zplus (Z_of_PeanoZ (Zpos p)) (Z_of_PeanoZ (Zneg q)). Proof. intros p q; simpl in |- *. rewrite <- hom_ord_mypcompare_pcompare in |- *. case (myPcompare p q); simpl in |- *. reflexivity. rewrite hom_myPminus_Pminus in |- *; reflexivity. rewrite hom_myPminus_Pminus in |- *; reflexivity. Qed. Lemma hom_PZplus_Zplus_negpos : forall p q:mypositive, Z_of_PeanoZ (Zplus (Zneg p) (Zpos q)) = ZArith.BinInt.Zplus (Z_of_PeanoZ (Zneg p)) (Z_of_PeanoZ (Zpos q)). Proof. intros p q; simpl in |- *. rewrite <- hom_ord_mypcompare_pcompare in |- *. case (myPcompare p q); simpl in |- *. reflexivity. rewrite hom_myPminus_Pminus in |- *; reflexivity. rewrite hom_myPminus_Pminus in |- *; reflexivity. Qed. Theorem hom_PZplus_Zplus : forall x y:Z, Z_of_PeanoZ (Zplus x y) = ZArith.BinInt.Zplus (Z_of_PeanoZ x)(Z_of_PeanoZ y). Proof. intros x y; case x; case y. simpl in |- *; reflexivity. simpl in |- *; reflexivity. simpl in |- *; reflexivity. simpl in |- *; reflexivity. intros; simpl in |- *; rewrite hom_myPplus_Pplus in |- *; reflexivity. intros; apply hom_PZplus_Zplus_posneg. simpl in |- *; reflexivity. intros; apply hom_PZplus_Zplus_negpos. intros; simpl in |- *; rewrite hom_myPplus_Pplus in |- *; reflexivity. Qed. Theorem hom_PZmult_Zmult : forall x y:Z, Z_of_PeanoZ (Zmult x y) = ZArith.BinInt.Zmult (Z_of_PeanoZ x)(Z_of_PeanoZ y). Proof. intros x y; case x; case y. simpl in |- *; reflexivity. intro; simpl in |- *; reflexivity. intro; simpl in |- *; reflexivity. intro; simpl in |- *; reflexivity. intro; simpl in |- *. intro; rewrite hom_myPmult_Pmult in |- *; reflexivity. intros; simpl in |- *. rewrite hom_myPmult_Pmult in |- *; reflexivity. intro; simpl in |- *; reflexivity. intros; simpl in |- *; rewrite hom_myPmult_Pmult in |- *; reflexivity. intros; simpl in |- *; rewrite hom_myPmult_Pmult in |- *; reflexivity. Qed. (**全単射*) (*inj*) Theorem PeanoZ_Z_injective : forall x:Z, PeanoZ_of_Z (Z_of_PeanoZ x) = x. Proof. intro x; case x; simpl in |- *; try reflexivity. intro; rewrite myP_P_injective in |- *; reflexivity. intro; rewrite myP_P_injective in |- *; reflexivity. Qed. (*Surj*) Theorem PeanoZ_Z_surjective : forall y:ZArith.BinInt.Z, Z_of_PeanoZ (PeanoZ_of_Z y) = y. Proof. intro y; case y; simpl in |- *; try reflexivity. intro; rewrite myP_P_surjective in |- *; reflexivity. intro; rewrite myP_P_surjective in |- *; reflexivity. Qed.