読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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.