Library Coq.Arith.PeanoNat
Implementation of NAxiomsSig by nat
Operations over nat are defined in a separate module
When including property functors, inline t eq zero one two lt le succ
All operations are well-defined (trivial here since eq is Leibniz)
Bi-directional induction.
Recursion function
Remaining constants not defined in Coq.Init.Nat
NB: Aliasing
le is mandatory, since only a Definition can implement
an interface Parameter...
Basic specifications : pred add sub mul
Decidability of equality over nat.
Ternary comparison
With
nat, it would be easier to prove first
compare_spec,
then the properties below. But then we wouldn't be able to
benefit from functor
BoolOrderFacts
Some more advanced properties of comparison and orders,
including compare_spec and lt_irrefl and lt_eq_cases.
We can now derive all properties of basic functions and orders,
and use these properties for proving the specs of more advanced
functions.
Lemma div2_double n :
div2 (2
*n)
= n.
Lemma div2_succ_double n :
div2 (
S (2
*n))
= n.
Lemma le_div2 n :
div2 (
S n)
<= n.
Lemma lt_div2 n : 0
< n -> div2 n < n.
Lemma div2_decr a n :
a <= S n -> div2 a <= n.
Lemma double_twice :
forall n,
double n = 2
*n.
Lemma testbit_0_l :
forall n,
testbit 0
n = false.
Lemma testbit_odd_0 a :
testbit (2
*a+1) 0
= true.
Lemma testbit_even_0 a :
testbit (2
*a) 0
= false.
Lemma testbit_odd_succ' a n :
testbit (2
*a+1) (
S n)
= testbit a n.
Lemma testbit_even_succ' a n :
testbit (2
*a) (
S n)
= testbit a n.
Lemma shiftr_specif :
forall a n m,
testbit (
shiftr a n)
m = testbit a (
m+n).
Lemma shiftl_specif_high :
forall a n 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 div2_bitwise :
forall op n a b,
div2 (
bitwise op (
S n)
a b)
= bitwise op n (
div2 a) (
div2 b).
Lemma odd_bitwise :
forall op n a b,
odd (
bitwise op (
S n)
a b)
= op (
odd a) (
odd b).
Lemma testbit_bitwise_1 :
forall op,
(forall b,
op false b = false) ->
forall n m a b,
a<=n ->
testbit (
bitwise op n a b)
m = op (
testbit a m) (
testbit b m).
Lemma testbit_bitwise_2 :
forall op,
op false false = false ->
forall n m a b,
a<=n -> b<=n ->
testbit (
bitwise op n a b)
m = op (
testbit a m) (
testbit b m).
Lemma land_spec a b n :
testbit (
land a b)
n = testbit a n && testbit b n.
Lemma ldiff_spec a b n :
testbit (
ldiff a b)
n = testbit a n && negb (
testbit b n).
Lemma lor_spec a b n :
testbit (
lor a b)
n = testbit a n || testbit b n.
Lemma lxor_spec a b n :
testbit (
lxor a b)
n = xorb (
testbit a n) (
testbit b n).
Lemma div2_spec a :
div2 a = shiftr a 1.
Aliases with extra dummy hypothesis, to fulfil the interface
Properties of advanced functions (pow, sqrt, log2, ...)
Properties of tail-recursive addition and multiplication
Re-export notations that should be available even when
the Nat module is not imported.
Infix "^" :=
Nat.pow :
nat_scope.
Infix "=?" :=
Nat.eqb (
at level 70) :
nat_scope.
Infix "<=?" :=
Nat.leb (
at level 70) :
nat_scope.
Infix "<?" :=
Nat.ltb (
at level 70) :
nat_scope.
Infix "?=" :=
Nat.compare (
at level 70) :
nat_scope.
Infix "/" :=
Nat.div :
nat_scope.
Infix "mod" :=
Nat.modulo (
at level 40,
no associativity) :
nat_scope.
Hint Unfold Nat.le :
core.
Hint Unfold Nat.lt :
core.
Nat contains an
order tactic for natural numbers
Note that
Nat.order is domain-agnostic: it will not prove
1<=2 or
x<=x+x, but rather things like
x<=y -> y<=x -> x=y.