Library Coq.Numbers.Cyclic.Abstract.NZCyclic
Require
Export
NZAxioms
.
Require
Import
ZArith
.
Require
Import
Zpow_facts
.
Require
Import
DoubleType
.
Require
Import
CyclicAxioms
.
Require
Import
Lia
.
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
eq
(
n
m
:
t
) :=
[|
n
|]
=
[|
m
|]
.
Definition
zero
:=
ZnZ.zero
.
Definition
one
:=
ZnZ.one
.
Definition
two
:=
ZnZ.succ
ZnZ.one
.
Definition
succ
:=
ZnZ.succ
.
Definition
pred
:=
ZnZ.pred
.
Definition
add
:=
ZnZ.add
.
Definition
sub
:=
ZnZ.sub
.
Definition
mul
:=
ZnZ.mul
.
Hint Rewrite
ZnZ.spec_0
ZnZ.spec_1
ZnZ.spec_succ
ZnZ.spec_pred
ZnZ.spec_add
ZnZ.spec_mul
ZnZ.spec_sub
:
cyclic
.
Ltac
zify
:=
unfold
eq
,
zero
,
one
,
two
,
succ
,
pred
,
add
,
sub
,
mul
in
*;
autorewrite
with
cyclic
.
Ltac
zcongruence
:=
repeat
red
;
intros
;
zify
;
congruence
.
Instance
eq_equiv
:
Equivalence
eq
.
Program Instance
succ_wd
:
Proper
(
eq
==>
eq
)
succ
.
Program Instance
pred_wd
:
Proper
(
eq
==>
eq
)
pred
.
Program Instance
add_wd
:
Proper
(
eq
==>
eq
==>
eq
)
add
.
Program Instance
sub_wd
:
Proper
(
eq
==>
eq
==>
eq
)
sub
.
Program Instance
mul_wd
:
Proper
(
eq
==>
eq
==>
eq
)
mul
.
Theorem
gt_wB_1
: 1
<
wB
.
Theorem
gt_wB_0
: 0
<
wB
.
Lemma
one_mod_wB
: 1
mod
wB
=
1.
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
.
Theorem
one_succ
:
one
==
succ
zero
.
Theorem
two_succ
:
two
==
succ
one
.
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
(
ZnZ.of_Z
n
).
Lemma
B0
:
B
0.
Lemma
BS
:
forall
n
:
Z
, 0
<=
n
->
n
<
wB
-
1
->
B
n
->
B
(
n
+
1).
Theorem
Zbounded_induction
:
(
forall
Q
:
Z
->
Prop
,
forall
b
:
Z
,
Q
0
->
(
forall
n
, 0
<=
n
->
n
<
b
-
1
->
Q
n
->
Q
(
n
+
1)
)
->
forall
n
, 0
<=
n
->
n
<
b
->
Q
n
)%
Z
.
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
.
Definition
t
:=
t
.
End
NZCyclicAxiomsMod
.