Library Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms
The interface ZSig.ZType implies the interface ZAxiomsSig
Module ZTypeIsZAxioms (
Import ZZ :
ZType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt
spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2
:
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.
Theorem one_succ : 1
== succ 0.
Theorem two_succ : 2
== succ 1.
Section Induction.
Variable A :
ZZ.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
Opp
Abs / Sgn
Power
Square
Sqrt
Log2
Even / Odd
Div / Mod
Quot / Rem
Gcd
Bitwise operations
Program Instance testbit_wd :
Proper (
eq==>eq==>Logic.eq)
testbit.
Lemma testbit_odd_0 :
forall a,
testbit (2
*a+1) 0
= true.
Lemma testbit_even_0 :
forall a,
testbit (2
*a) 0
= false.
Lemma testbit_odd_succ :
forall a n, 0
<=n ->
testbit (2
*a+1) (
succ n)
= testbit a n.
Lemma testbit_even_succ :
forall a n, 0
<=n ->
testbit (2
*a) (
succ n)
= testbit a n.
Lemma testbit_neg_r :
forall a n,
n<0 ->
testbit a n = false.
Lemma shiftr_spec :
forall a n m, 0
<=m ->
testbit (
shiftr a n)
m = testbit a (
m+n).
Lemma shiftl_spec_high :
forall a n m, 0
<=m ->
n<=m ->
testbit (
shiftl a n)
m = testbit a (
m-n).
Lemma shiftl_spec_low :
forall a n m,
m<n ->
testbit (
shiftl a n)
m = false.
Lemma land_spec :
forall a b n,
testbit (
land a b)
n = testbit a n && testbit b n.
Lemma lor_spec :
forall a b n,
testbit (
lor a b)
n = testbit a n || testbit b n.
Lemma ldiff_spec :
forall a b n,
testbit (
ldiff a b)
n = testbit a n && negb (
testbit b n).
Lemma lxor_spec :
forall a b n,
testbit (
lxor a b)
n = xorb (
testbit a n) (
testbit b n).
Lemma div2_spec :
forall a,
div2 a == shiftr a 1.
End ZTypeIsZAxioms.
Module ZType_ZAxioms (
ZZ :
ZType)
<:
ZAxiomsSig <:
OrderFunctions ZZ <:
HasMinMax ZZ
:=
ZZ <+
ZTypeIsZAxioms.