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.