# PeanoZArith.v

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