Library Coq.Numbers.Natural.SpecViaZ.NSigNAxioms
The interface NSig.NType implies the interface NAxiomsSig
Module NTypeIsNAxioms (
Import NN :
NType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
spec_square spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N
spec_pow spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
:
nsimpl.
Ltac nsimpl :=
autorewrite with nsimpl.
Ltac ncongruence :=
unfold eq,
to_N;
repeat red;
intros;
nsimpl;
congruence.
Ltac zify :=
unfold eq,
lt,
le,
to_N in *;
nsimpl.
Ltac omega_pos n :=
generalize (
spec_pos n);
omega with *.
Local Obligation Tactic :=
ncongruence.
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 pred_succ :
forall n,
pred (
succ n)
== n.
Theorem one_succ : 1
== succ 0.
Theorem two_succ : 2
== succ 1.
Definition N_of_Z z :=
of_N (
Z.to_N z).
Lemma spec_N_of_Z z : (0
<=z)%
Z ->
[N_of_Z z] = z.
Section Induction.
Variable A :
NN.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 (
N_of_Z z).
Lemma B0 :
B 0.
Lemma BS :
forall z :
Z, (0
<= z)%
Z ->
B z ->
B (
z + 1).
Lemma B_holds :
forall z :
Z, (0
<= 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
Properties specific to natural numbers, not integers.
Power
Square
Sqrt
Log2
Even / Odd
Div / Mod
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.
Recursion