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.
Local Open Scope Z_scope.
Definition t :=
w.
Definition NZ_to_Z :
t ->
Z :=
znz_to_Z w_op.
Definition Z_to_NZ :
Z ->
t :=
znz_of_Z w_op.
Local Notation wB := (
base w_op.(
znz_digits)).
Local Notation "[| x |]" := (
w_op.(
znz_to_Z)
x) (
at level 0,
x at level 99).
Definition eq (
n m :
t) :=
[| n |] = [| m |].
Definition zero :=
w_op.(
znz_0).
Definition succ :=
w_op.(
znz_succ).
Definition pred :=
w_op.(
znz_pred).
Definition add :=
w_op.(
znz_add).
Definition sub :=
w_op.(
znz_sub).
Definition mul :=
w_op.(
znz_mul).
Local Infix "==" :=
eq (
at level 70).
Local Notation "0" :=
zero.
Local Notation S :=
succ.
Local Notation P :=
pred.
Local Infix "+" :=
add.
Local Infix "-" :=
sub.
Local Infix "*" :=
mul.
Hint Rewrite w_spec.(
spec_0)
w_spec.(
spec_succ)
w_spec.(
spec_pred)
w_spec.(
spec_add)
w_spec.(
spec_mul)
w_spec.(
spec_sub) :
w.
Ltac wsimpl :=
unfold eq,
zero,
succ,
pred,
add,
sub,
mul;
autorewrite with w.
Ltac wcongruence :=
repeat red;
intros;
wsimpl;
congruence.
Instance eq_equiv :
Equivalence eq.
Instance succ_wd :
Proper (
eq ==> eq)
succ.
Instance pred_wd :
Proper (
eq ==> eq)
pred.
Instance add_wd :
Proper (
eq ==> eq ==> eq)
add.
Instance sub_wd :
Proper (
eq ==> eq ==> eq)
sub.
Instance mul_wd :
Proper (
eq ==> eq ==> eq)
mul.
Theorem gt_wB_1 : 1
< wB.
Theorem gt_wB_0 : 0
< wB.
Lemma succ_mod_wB :
forall n :
Z,
(n + 1
) mod wB = ((n mod wB) + 1
) mod wB.
Lemma pred_mod_wB :
forall n :
Z,
(n - 1
) mod wB = ((n mod wB) - 1
) mod wB.
Lemma NZ_to_Z_mod :
forall n,
[| n |] mod wB = [| n |].
Theorem pred_succ :
forall n,
P (
S n)
== n.
Lemma Z_to_NZ_0 :
Z_to_NZ 0%
Z == 0.
Section Induction.
Variable A :
t ->
Prop.
Hypothesis A_wd :
Proper (
eq ==> iff)
A.
Hypothesis A0 :
A 0.
Hypothesis AS :
forall n,
A n <-> A (
S n).
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 bi_induction :
forall n,
A n.
End Induction.
Theorem add_0_l :
forall n, 0
+ n == n.
Theorem add_succ_l :
forall n m,
(S n) + m == S (
n + m).
Theorem sub_0_r :
forall n,
n - 0
== n.
Theorem sub_succ_r :
forall n m,
n - (S m) == P (
n - m).
Theorem mul_0_l :
forall n, 0
* n == 0.
Theorem mul_succ_l :
forall n m,
(S n) * m == n * m + m.
End NZCyclicAxiomsMod.