Library Coq.Numbers.Integer.NatPairs.ZNatPairs



Require Import NSub.
Require Export ZMulOrder.
Require Export Ring.

Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
Module Import NPropMod := NSubPropFunct NAxiomsMod.


Open Local Scope NatScope.

Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq.

Add Ring NSR : Nsemi_ring.


Definition Z := (N * N)%type.
Definition Z0 : Z := (0, 0).
Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
Definition Zpred (n : Z) : Z := (fst n, S (snd n)).


Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).


Definition Zmul (n m : Z) : Z :=
  ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).

Delimit Scope IntScope with Int.
Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
Notation "0" := Z0 : IntScope.
Notation "1" := (Zsucc Z0) : IntScope.
Notation "x + y" := (Zadd x y) : IntScope.
Notation "x - y" := (Zsub x y) : IntScope.
Notation "x * y" := (Zmul x y) : IntScope.
Notation "x < y" := (Zlt x y) : IntScope.
Notation "x <= y" := (Zle x y) : IntScope.
Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
Notation "x >= y" := (Zle y x) (only parsing) : IntScope.

Notation Local N := NZ.
Notation Local NE := NZeq (only parsing).
Notation Local add_wd := NZadd_wd (only parsing).

Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
Module Export NZAxiomsMod <: NZAxiomsSig.

Definition NZ : Type := Z.
Definition NZeq := Zeq.
Definition NZ0 := Z0.
Definition NZsucc := Zsucc.
Definition NZpred := Zpred.
Definition NZadd := Zadd.
Definition NZsub := Zsub.
Definition NZmul := Zmul.

Theorem ZE_refl : reflexive Z Zeq.


Theorem ZE_sym : symmetric Z Zeq.

Theorem ZE_trans : transitive Z Zeq.


Theorem NZeq_equiv : equiv Z Zeq.

Add Relation Z Zeq
 reflexivity proved by (proj1 NZeq_equiv)
 symmetry proved by (proj2 (proj2 NZeq_equiv))
 transitivity proved by (proj1 (proj2 NZeq_equiv))
as NZeq_rel.

Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.

Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.

Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.

Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.

Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd.

Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.

Section Induction.
Open Scope NatScope.
Variable A : Z -> Prop.
Hypothesis A_wd : predicate_wd Zeq A.

Add Morphism A with signature Zeq ==> iff as A_morph.

Theorem NZinduction :
  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.





End Induction.


Open Local Scope IntScope.

Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.

Theorem NZadd_0_l : forall n : Z, 0 + n == n.


Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).


Theorem NZsub_0_r : forall n : Z, n - 0 == n.


Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).


Theorem NZmul_0_l : forall n : Z, 0 * n == 0.


Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.


End NZAxiomsMod.

Definition NZlt := Zlt.
Definition NZle := Zle.
Definition NZmin := Zmin.
Definition NZmax := Zmax.

Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.




Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.


Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.



Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.



Open Local Scope IntScope.

Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.


Theorem NZlt_irrefl : forall n : Z, ~ (n < n).


Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m.


Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.


Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.


Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.


Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.


End NZOrdAxiomsMod.

Definition Zopp (n : Z) : Z := (snd n, fst n).

Notation "- x" := (Zopp x) : IntScope.

Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.


Open Local Scope IntScope.

Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.

Theorem Zopp_0 : - 0 == 0.


Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).

End ZPairsAxiomsMod.