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)
Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
#[global]
Program Instance succ_wd : Proper (eq==>eq) S.
#[global]
Program Instance pred_wd : Proper (eq==>eq) pred.
#[global]
Program Instance add_wd : Proper (eq==>eq==>eq) plus.
#[global]
Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
#[global]
Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
#[global]
Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
#[global]
Program Instance div_wd : Proper (eq==>eq==>eq) div.
#[global]
Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
#[global]
Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
#[global]
Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.
Bi-directional induction.
Theorem bi_induction :
forall A : nat -> Prop, Proper (eq==>iff) A ->
A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
Recursion function
Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
nat_rect (fun _ => A).
#[global]
Instance recursion_wd {A} (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
Theorem recursion_0 :
forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.
Theorem recursion_succ :
forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
Remaining constants not defined in Coq.Init.Nat
Lemma pred_succ n : pred (S n) = n.
Lemma pred_0 : pred 0 = 0.
Lemma one_succ : 1 = S 0.
Lemma two_succ : 2 = S 1.
Lemma add_0_l n : 0 + n = n.
Lemma add_succ_l n m : (S n) + m = S (n + m).
Lemma sub_0_r n : n - 0 = n.
Lemma sub_succ_r n m : n - (S m) = pred (n - m).
Lemma mul_0_l n : 0 * n = 0.
Lemma mul_succ_l n m : S n * m = n * m + m.
Lemma lt_succ_r n m : n < S m <-> n <= m.
Lemma eqb_eq n m : eqb n m = true <-> n = m.
Lemma leb_le n m : (n <=? m) = true <-> n <= m.
Lemma ltb_lt n m : (n <? m) = true <-> n < m.
Ternary comparison
Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
Lemma max_l : forall n m, m <= n -> max n m = n.
Lemma max_r : forall n m, n <= m -> max n m = m.
Lemma min_l : forall n m, n <= m -> min n m = n.
Lemma min_r : forall n m, m <= n -> min n m = m.
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 pow_neg_r a b : b<0 -> a^b = 0.
Lemma pow_0_r a : a^0 = 1.
Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b.
Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.
Module Private_Parity.
Lemma Even_1 : ~ Even 1.
Lemma Even_2 n : Even n <-> Even (S (S n)).
Lemma Odd_0 : ~ Odd 0.
Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
End Private_Parity.
Import Private_Parity.
Lemma even_spec : forall n, even n = true <-> Even n.
Lemma odd_spec : forall n, odd n = true <-> Odd n.
Lemma divmod_spec : forall x y q u, u <= y ->
let (q',u') := divmod x y q u in
x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.
Lemma div_mod_eq x y : x = y*(x/y) + x mod y.
Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.
Lemma sqrt_iter_spec : forall k p q r,
q = p+p -> r<=q ->
let s := sqrt_iter k p q r in
s*s <= k + p*p + (q - r) < (S s)*(S s).
Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a.
Lemma sqrt_neg a : a<0 -> sqrt a = 0.
Lemma log2_iter_spec : forall k p q r,
2^(S p) = q + S r -> r < 2^p ->
let s := log2_iter k p q r in
2^s <= k + q < 2^(S s).
Lemma log2_spec n : 0<n ->
2^(log2 n) <= n < 2^(S (log2 n)).
Lemma log2_nonpos n : n<=0 -> log2 n = 0.
Definition divide x y := exists z, y=z*x.
Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
Lemma gcd_divide_l : forall a b, (gcd a b | a).
Lemma gcd_divide_r : forall a b, (gcd a b | b).
Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
Lemma gcd_nonneg a b : 0<=gcd a b.
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
Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n.
Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n.
Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m.
Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
Properties of advanced functions (pow, sqrt, log2, ...)
Properties of tail-recursive addition and multiplication
Lemma tail_add_spec n m : tail_add n m = n + m.
Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m.
Lemma tail_mul_spec n m : tail_mul n m = n * m.
End Nat.
Re-export notations that should be available even when
the Nat module is not imported.
Bind Scope nat_scope with Nat.t nat.
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.
#[global]
Hint Unfold Nat.le : core.
#[global]
Hint Unfold Nat.lt : core.
Register Nat.le_trans as num.nat.le_trans.
Register Nat.nlt_0_r as num.nat.nlt_0_r.
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.