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.