Library Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms
The interface ZSig.ZType implies the interface ZAxiomsSig
It also provides
sgn,
abs,
div,
mod
Module ZTypeIsZAxioms (
Import Z :
ZType').
Hint Rewrite
spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo
spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
:
zsimpl.
Ltac zsimpl :=
autorewrite with zsimpl.
Ltac zcongruence :=
repeat red;
intros;
zsimpl;
congruence.
Ltac zify :=
unfold eq,
lt,
le in *;
zsimpl.
Instance eq_equiv :
Equivalence eq.
Local Obligation Tactic :=
zcongruence.
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 pred_succ :
forall n,
pred (
succ n)
== n.
Section Induction.
Variable A :
Z.t ->
Prop.
Hypothesis A_wd :
Proper (
eq==>iff)
A.
Hypothesis A0 :
A 0.
Hypothesis AS :
forall n,
A n <-> A (
succ n).
Let B (
z :
Z) :=
A (
of_Z z).
Lemma B0 :
B 0.
Lemma BS :
forall z :
Z,
B z ->
B (
z + 1).
Lemma BP :
forall z :
Z,
B z ->
B (
z - 1).
Lemma B_holds :
forall z :
Z,
B z.
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,
(succ n) + m == succ (
n + m).
Theorem sub_0_r :
forall n,
n - 0
== n.
Theorem sub_succ_r :
forall n m,
n - (succ m) == pred (
n - m).
Theorem mul_0_l :
forall n, 0
* n == 0.
Theorem mul_succ_l :
forall n m,
(succ n) * m == n * m + m.
Order
Part specific to integers, not natural numbers
Program Instance opp_wd :
Proper (
eq ==> eq)
opp.
Theorem succ_pred :
forall n,
succ (
pred n)
== n.
Theorem opp_0 :
- 0
== 0.
Theorem opp_succ :
forall n,
- (succ n) == pred (
- n).
Theorem abs_eq :
forall n, 0
<= n ->
abs n == n.
Theorem abs_neq :
forall n,
n <= 0 ->
abs n == -n.
Theorem sgn_null :
forall n,
n==0 ->
sgn n == 0.
Theorem sgn_pos :
forall n, 0
<n ->
sgn n == succ 0.
Theorem sgn_neg :
forall n,
n<0 ->
sgn n == opp (
succ 0).
Program Instance div_wd :
Proper (
eq==>eq==>eq)
div.
Program Instance mod_wd :
Proper (
eq==>eq==>eq)
modulo.
Theorem div_mod :
forall a b,
~b==0 ->
a == b*(div a b) + (modulo a b).
Theorem mod_pos_bound :
forall a b, 0
< b -> 0
<= modulo a b /\ modulo a b < b.
Theorem mod_neg_bound :
forall a b,
b < 0 ->
b < modulo a b /\ modulo a b <= 0.
End ZTypeIsZAxioms.
Module ZType_ZAxioms (
Z :
ZType)
<:
ZAxiomsSig <:
ZDivSig <:
HasCompare Z <:
HasEqBool Z <:
HasMinMax Z
:=
Z <+
ZTypeIsZAxioms.