Library Coq.Numbers.Cyclic.Abstract.NZCyclic
From CyclicType to NZAxiomsSig
A Z/nZ representation given by a module type CyclicType
implements NZAxiomsSig, e.g. the common properties between
N and Z with no ordering. Notice that the n in Z/nZ is
a power of 2.
Module NZCyclicAxiomsMod (
Import Cyclic :
CyclicType) <:
NZAxiomsSig.
Open Local Scope Z_scope.
Definition NZ :=
w.
Definition NZ_to_Z :
NZ ->
Z :=
znz_to_Z w_op.
Definition Z_to_NZ :
Z ->
NZ :=
znz_of_Z w_op.
Notation Local wB := (
base w_op.(
znz_digits)).
Notation Local "[| x |]" := (
w_op.(
znz_to_Z)
x) (
at level 0,
x at level 99).
Definition NZeq (
n m :
NZ) := [|
n |] = [|
m |].
Definition NZ0 :=
w_op.(
znz_0).
Definition NZsucc :=
w_op.(
znz_succ).
Definition NZpred :=
w_op.(
znz_pred).
Definition NZadd :=
w_op.(
znz_add).
Definition NZsub :=
w_op.(
znz_sub).
Definition NZmul :=
w_op.(
znz_mul).
Theorem NZeq_equiv :
equiv NZ NZeq.
Add Relation NZ NZeq
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 NZsucc with signature NZeq ==>
NZeq as NZsucc_wd.
Add Morphism NZpred with signature NZeq ==>
NZeq as NZpred_wd.
Add Morphism NZadd with signature NZeq ==>
NZeq ==>
NZeq as NZadd_wd.
Add Morphism NZsub with signature NZeq ==>
NZeq ==>
NZeq as NZsub_wd.
Add Morphism NZmul with signature NZeq ==>
NZeq ==>
NZeq as NZmul_wd.
Delimit Scope IntScope with Int.
Open Local Scope IntScope.
Notation "x == y" := (
NZeq x y) (
at level 70) :
IntScope.
Notation "x ~= y" := (~
NZeq x y) (
at level 70) :
IntScope.
Notation "0" :=
NZ0 :
IntScope.
Notation S x := (
NZsucc x).
Notation P x := (
NZpred x).
Notation "x + y" := (
NZadd x y) :
IntScope.
Notation "x - y" := (
NZsub x y) :
IntScope.
Notation "x * y" := (
NZmul x y) :
IntScope.
Theorem gt_wB_1 : 1 <
wB.
Theorem gt_wB_0 : 0 <
wB.
Lemma NZsucc_mod_wB :
forall n :
Z, (
n + 1)
mod wB = ((
n mod wB) + 1)
mod wB.
Lemma NZpred_mod_wB :
forall n :
Z, (
n - 1)
mod wB = ((
n mod wB) - 1)
mod wB.
Lemma NZ_to_Z_mod :
forall n :
NZ, [|
n |]
mod wB = [|
n |].
Theorem NZpred_succ :
forall n :
NZ,
P (
S n) ==
n.
Lemma Z_to_NZ_0 :
Z_to_NZ 0%Z == 0%Int.
Section Induction.
Variable A :
NZ ->
Prop.
Hypothesis A_wd :
predicate_wd NZeq A.
Hypothesis A0 :
A 0.
Hypothesis AS :
forall n :
NZ,
A n <->
A (
S n).
Add Morphism A with signature NZeq ==>
iff as A_morph.
Let B (
n :
Z) :=
A (
Z_to_NZ n).
Lemma B0 :
B 0.
Lemma BS :
forall n :
Z, 0 <=
n ->
n <
wB - 1 ->
B n ->
B (
n + 1).
Lemma B_holds :
forall n :
Z, 0 <=
n <
wB ->
B n.
Theorem NZinduction :
forall n :
NZ,
A n.
End Induction.
Theorem NZadd_0_l :
forall n :
NZ, 0 +
n ==
n.
Theorem NZadd_succ_l :
forall n m :
NZ, (
S n) +
m ==
S (
n +
m).
Theorem NZsub_0_r :
forall n :
NZ,
n - 0 ==
n.
Theorem NZsub_succ_r :
forall n m :
NZ,
n - (
S m) ==
P (
n -
m).
Theorem NZmul_0_l :
forall n :
NZ, 0 *
n == 0.
Theorem NZmul_succ_l :
forall n m :
NZ, (
S n) *
m ==
n *
m +
m.
End NZCyclicAxiomsMod.