Library Coq.NArith.BinNat


Require Export BinNums.
Require Import BinPos RelationClasses Morphisms Setoid
 Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties.
Require BinNatDef.

Binary natural numbers, operations and properties

The type N and its constructors N0 and Npos are now defined in BinNums.v
Every definitions and properties about binary natural numbers are placed in a module N for qualification purpose.

Local Open Scope N_scope.

Every definitions and early properties about positive numbers are placed in a module N for qualification purpose.

Module N
 <: NAxiomsSig
 <: UsualOrderedTypeFull
 <: UsualDecidableTypeFull
 <: TotalOrder.

Definitions of operations, now in a separate file

Include BinNatDef.N.

When including property functors, only inline t eq zero one two


Logical predicates

Definition eq := @Logic.eq N.
Definition eq_equiv := @eq_equivalence N.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : N_scope.
Infix "<" := lt : N_scope.
Infix ">=" := ge : N_scope.
Infix ">" := gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Definition divide p q := exists r, q = r*p.
Notation "( p | q )" := (divide p q) (at level 0) : N_scope.

Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.

Decidability of equality.

Definition eq_dec : forall n m : N, { n = m } + { n <> m }.

Discrimination principle

Definition discr n : { p:positive | n = pos p } + { n = 0 }.

Convenient induction principles

Definition binary_rect (P:N -> Type) (f0 : P 0)
  (f2 : forall n, P n -> P (double n))
  (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n :=
 let P´ p := P (pos p) in
 let f2´ p := f2 (pos p) in
 let fS2´ p := fS2 (pos p) in
 match n with
 | 0 => f0
 | pos p => positive_rect P´ fS2´ f2´ (fS2 0 f0) p
 end.

Definition binary_rec (P:N -> Set) := binary_rect P.
Definition binary_ind (P:N -> Prop) := binary_rect P.

Peano induction on binary natural numbers

Definition peano_rect
  (P : N -> Type) (f0 : P 0)
    (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
let P´ p := P (pos p) in
let f´ p := f (pos p) in
match n with
| 0 => f0
| pos p => Pos.peano_rect P´ (f 0 f0) f´ p
end.

Theorem peano_rect_base P a f : peano_rect P a f 0 = a.

Theorem peano_rect_succ P a f n :
 peano_rect P a f (succ n) = f n (peano_rect P a f n).

Definition peano_ind (P : N -> Prop) := peano_rect P.

Definition peano_rec (P : N -> Set) := peano_rect P.

Theorem peano_rec_base P a f : peano_rec P a f 0 = a.

Theorem peano_rec_succ P a f n :
 peano_rec P a f (succ n) = f n (peano_rec P a f n).

Properties of mixed successor and predecessor.

Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).

Lemma succ_pos_spec n : pos (succ_pos n) = succ n.

Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n.

Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.

Properties of successor and predecessor

Theorem pred_succ n : pred (succ n) = n.

Theorem pred_sub n : pred n = sub n 1.

Theorem succ_0_discr n : succ n <> 0.

Specification of addition

Theorem add_0_l n : 0 + n = n.

Theorem add_succ_l n m : succ n + m = succ (n + m).

Specification of subtraction.

Theorem sub_0_r n : n - 0 = n.

Theorem sub_succ_r n m : n - succ m = pred (n - m).

Specification of multiplication

Theorem mul_0_l n : 0 * n = 0.

Theorem mul_succ_l n m : (succ n) * m = n * m + m.

Specification of boolean comparisons.

Lemma eqb_eq n m : eqb n m = true <-> n=m.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.

Basic properties of comparison

Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.

Theorem compare_lt_iff n m : (n ?= m) = Lt <-> n < m.

Theorem compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.

Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m).

Some more advanced properties of comparison and orders, including compare_spec and lt_irrefl and lt_eq_cases.

Include BoolOrderFacts.

We regroup here some results used for proving the correctness of more advanced functions. These results will also be provided by the generic functor of properties about natural numbers instantiated at the end of the file.

Module Import Private_BootStrap.

Theorem add_0_r n : n + 0 = n.

Theorem add_comm n m : n + m = m + n.

Theorem add_assoc n m p : n + (m + p) = n + m + p.

Lemma sub_add n m : n <= m -> m - n + n = m.

Theorem mul_comm n m : n * m = m * n.

Lemma le_0_l n : 0<=n.

Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).

Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m.

End Private_BootStrap.

Specification of lt and le.

Lemma lt_succ_r n m : n < succ m <-> n<=m.

Properties of double and succ_double

Lemma double_spec n : double n = 2 * n.

Lemma succ_double_spec n : succ_double n = 2 * n + 1.

Lemma double_add n m : double (n+m) = double n + double m.

Lemma succ_double_add n m : succ_double (n+m) = double n + succ_double m.

Lemma double_mul n m : double (n*m) = double n * m.

Lemma succ_double_mul n m :
 succ_double n * m = double n * m + m.

Lemma div2_double n : div2 (double n) = n.

Lemma div2_succ_double n : div2 (succ_double n) = n.

Lemma double_inj n m : double n = double m -> n = m.

Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m.

Lemma succ_double_lt n m : n<m -> succ_double n < double m.

Specification of minimum and maximum

Theorem min_l n m : n <= m -> min n m = n.

Theorem min_r n m : m <= n -> min n m = m.

Theorem max_l n m : m <= n -> max n m = n.

Theorem max_r n m : n <= m -> max n m = m.

0 is the least natural number

Theorem compare_0_r n : (n ?= 0) <> Lt.

Specifications of power

Lemma pow_0_r n : n ^ 0 = 1.

Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p.

Lemma pow_neg_r n p : p<0 -> n^p = 0.

Specification of square

Lemma square_spec n : square n = n * n.

Specification of Base-2 logarithm

Lemma size_log2 n : n<>0 -> size n = succ (log2 n).

Lemma size_gt n : n < 2^(size n).

Lemma size_le n : 2^(size n) <= succ_double n.

Lemma log2_spec n : 0 < n ->
 2^(log2 n) <= n < 2^(succ (log2 n)).

Lemma log2_nonpos n : n<=0 -> log2 n = 0.

Specification of parity functions

Lemma even_spec n : even n = true <-> Even n.

Lemma odd_spec n : odd n = true <-> Odd n.

Specification of the euclidean division

Theorem pos_div_eucl_spec (a:positive)(b:N) :
  let (q,r) := pos_div_eucl a b in pos a = q * b + r.

Theorem div_eucl_spec a b :
 let (q,r) := div_eucl a b in a = b * q + r.

Theorem div_mod´ a b : a = b * (a/b) + (a mod b).

Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b).

Theorem pos_div_eucl_remainder (a:positive) (b:N) :
  b<>0 -> snd (pos_div_eucl a b) < b.

Theorem mod_lt a b : b<>0 -> a mod b < b.

Theorem mod_bound_pos a b : 0<=a -> 0<b -> 0 <= a mod b < b.

Specification of square root

Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.

Lemma sqrtrem_spec n :
 let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s.

Lemma sqrt_spec n : 0<=n ->
 let s := sqrt n in s*s <= n < (succ s)*(succ s).

Lemma sqrt_neg n : n<0 -> sqrt n = 0.

Specification of gcd
The first component of ggcd is gcd

Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.

The other components of ggcd are indeed the correct factors.

Lemma ggcd_correct_divisors a b :
  let ´(g,(aa,bb)) := ggcd a b in
  a=g*aa /\ b=g*bb.

We can use this fact to prove a part of the gcd correctness

Lemma gcd_divide_l a b : (gcd a b | a).

Lemma gcd_divide_r a b : (gcd a b | b).

We now prove directly that gcd is the greatest amongst common divisors

Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b).

Lemma gcd_nonneg a b : 0 <= gcd a b.

Specification of bitwise functions
Correctness proofs for testbit.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.

Lemma testbit_succ_r_div2 a n : 0<=n ->
 testbit a (succ n) = testbit (div2 a) n.

Lemma testbit_odd_succ a n : 0<=n ->
 testbit (2*a+1) (succ n) = testbit a n.

Lemma testbit_even_succ a n : 0<=n ->
 testbit (2*a) (succ n) = testbit a n.

Lemma testbit_neg_r a n : n<0 -> testbit a n = false.

Correctness proofs for shifts

Lemma shiftr_succ_r a n :
 shiftr a (succ n) = div2 (shiftr a n).

Lemma shiftl_succ_r a n :
 shiftl a (succ n) = double (shiftl a n).

Lemma shiftr_spec a n m : 0<=m ->
 testbit (shiftr a n) m = testbit a (m+n).

Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
 testbit (shiftl a n) m = testbit a (m-n).

Lemma shiftl_spec_low a n m : m<n ->
 testbit (shiftl a n) m = false.

Definition div2_spec a : div2 a = shiftr a 1.

Semantics of bitwise operations

Lemma pos_lxor_spec p p´ n :
 testbit (Pos.lxor p p´) n = xorb (Pos.testbit p n) (Pos.testbit p´ n).

Lemma lxor_spec a a´ n :
 testbit (lxor a a´) n = xorb (testbit a n) (testbit a´ n).

Lemma pos_lor_spec p p´ n :
 Pos.testbit (Pos.lor p p´) n = (Pos.testbit p n) || (Pos.testbit p´ n).

Lemma lor_spec a a´ n :
 testbit (lor a a´) n = (testbit a n) || (testbit a´ n).

Lemma pos_land_spec p p´ n :
 testbit (Pos.land p p´) n = (Pos.testbit p n) && (Pos.testbit p´ n).

Lemma land_spec a a´ n :
 testbit (land a a´) n = (testbit a n) && (testbit a´ n).

Lemma pos_ldiff_spec p p´ n :
 testbit (Pos.ldiff p p´) n = (Pos.testbit p n) && negb (Pos.testbit p´ n).

Lemma ldiff_spec a a´ n :
 testbit (ldiff a a´) n = (testbit a n) && negb (testbit a´ n).

Specification of constants

Lemma one_succ : 1 = succ 0.

Lemma two_succ : 2 = succ 1.

Definition pred_0 : pred 0 = 0.

Proofs of morphisms, obvious since eq is Leibniz

Local Obligation Tactic := simpl_relation.
Program Definition succ_wd : Proper (eq==>eq) succ := _.
Program Definition pred_wd : Proper (eq==>eq) pred := _.
Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.

Generic induction / recursion

Theorem bi_induction :
  forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.

Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
  peano_rect (fun _ => A).

Instance recursion_wd {A} (Aeq : relation A) :
 Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.

Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.

Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
 Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
  forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).

Instantiation of generic properties of natural numbers
The Bind Scope prevents N to stay associated with abstract_scope. (TODO FIX)

Include NProp. Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

In generic statements, the predicates lt and le have been favored, whereas gt and ge don't even exist in the abstract layers. The use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.

Lemma gt_lt_iff n m : n > m <-> m < n.

Lemma gt_lt n m : n > m -> m < n.

Lemma lt_gt n m : n < m -> m > n.

Lemma ge_le_iff n m : n >= m <-> m <= n.

Lemma ge_le n m : n >= m -> m <= n.

Lemma le_ge n m : n <= m -> m >= n.

Auxiliary results about right shift on positive numbers, used in BinInt

Lemma pos_pred_shiftl_low : forall p n m, m<n ->
 testbit (Pos.pred_N (Pos.shiftl p n)) m = true.

Lemma pos_pred_shiftl_high : forall p n m, n<=m ->
 testbit (Pos.pred_N (Pos.shiftl p n)) m =
 testbit (shiftl (Pos.pred_N p) n) m.

Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p).

End N.

Exportation of notations

Infix "+" := N.add : N_scope.
Infix "-" := N.sub : N_scope.
Infix "*" := N.mul : N_scope.
Infix "^" := N.pow : N_scope.

Infix "?=" := N.compare (at level 70, no associativity) : N_scope.

Infix "<=" := N.le : N_scope.
Infix "<" := N.lt : N_scope.
Infix ">=" := N.ge : N_scope.
Infix ">" := N.gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Infix "=?" := N.eqb (at level 70, no associativity) : N_scope.
Infix "<=?" := N.leb (at level 70, no associativity) : N_scope.
Infix "<?" := N.ltb (at level 70, no associativity) : N_scope.

Infix "/" := N.div : N_scope.
Infix "mod" := N.modulo (at level 40, no associativity) : N_scope.

Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope.

Compatibility notations

Notation N_rect := N_rect (only parsing).
Notation N_rec := N_rec (only parsing).
Notation N_ind := N_ind (only parsing).
Notation N0 := N0 (only parsing).
Notation Npos := N.pos (only parsing).

Notation Ndiscr := N.discr (compat "8.3").
Notation Ndouble_plus_one := N.succ_double (compat "8.3").
Notation Ndouble := N.double (compat "8.3").
Notation Nsucc := N.succ (compat "8.3").
Notation Npred := N.pred (compat "8.3").
Notation Nsucc_pos := N.succ_pos (compat "8.3").
Notation Ppred_N := Pos.pred_N (compat "8.3").
Notation Nplus := N.add (compat "8.3").
Notation Nminus := N.sub (compat "8.3").
Notation Nmult := N.mul (compat "8.3").
Notation Neqb := N.eqb (compat "8.3").
Notation Ncompare := N.compare (compat "8.3").
Notation Nlt := N.lt (compat "8.3").
Notation Ngt := N.gt (compat "8.3").
Notation Nle := N.le (compat "8.3").
Notation Nge := N.ge (compat "8.3").
Notation Nmin := N.min (compat "8.3").
Notation Nmax := N.max (compat "8.3").
Notation Ndiv2 := N.div2 (compat "8.3").
Notation Neven := N.even (compat "8.3").
Notation Nodd := N.odd (compat "8.3").
Notation Npow := N.pow (compat "8.3").
Notation Nlog2 := N.log2 (compat "8.3").

Notation nat_of_N := N.to_nat (compat "8.3").
Notation N_of_nat := N.of_nat (compat "8.3").
Notation N_eq_dec := N.eq_dec (compat "8.3").
Notation Nrect := N.peano_rect (compat "8.3").
Notation Nrect_base := N.peano_rect_base (compat "8.3").
Notation Nrect_step := N.peano_rect_succ (compat "8.3").
Notation Nind := N.peano_ind (compat "8.3").
Notation Nrec := N.peano_rec (compat "8.3").
Notation Nrec_base := N.peano_rec_base (compat "8.3").
Notation Nrec_succ := N.peano_rec_succ (compat "8.3").

Notation Npred_succ := N.pred_succ (compat "8.3").
Notation Npred_minus := N.pred_sub (compat "8.3").
Notation Nsucc_pred := N.succ_pred (compat "8.3").
Notation Ppred_N_spec := N.pos_pred_spec (compat "8.3").
Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.3").
Notation Ppred_Nsucc := N.pos_pred_succ (compat "8.3").
Notation Nplus_0_l := N.add_0_l (compat "8.3").
Notation Nplus_0_r := N.add_0_r (compat "8.3").
Notation Nplus_comm := N.add_comm (compat "8.3").
Notation Nplus_assoc := N.add_assoc (compat "8.3").
Notation Nplus_succ := N.add_succ_l (compat "8.3").
Notation Nsucc_0 := N.succ_0_discr (compat "8.3").
Notation Nsucc_inj := N.succ_inj (compat "8.3").
Notation Nminus_N0_Nle := N.sub_0_le (compat "8.3").
Notation Nminus_0_r := N.sub_0_r (compat "8.3").
Notation Nminus_succ_r:= N.sub_succ_r (compat "8.3").
Notation Nmult_0_l := N.mul_0_l (compat "8.3").
Notation Nmult_1_l := N.mul_1_l (compat "8.3").
Notation Nmult_1_r := N.mul_1_r (compat "8.3").
Notation Nmult_comm := N.mul_comm (compat "8.3").
Notation Nmult_assoc := N.mul_assoc (compat "8.3").
Notation Nmult_plus_distr_r := N.mul_add_distr_r (compat "8.3").
Notation Neqb_eq := N.eqb_eq (compat "8.3").
Notation Nle_0 := N.le_0_l (compat "8.3").
Notation Ncompare_refl := N.compare_refl (compat "8.3").
Notation Ncompare_Eq_eq := N.compare_eq (compat "8.3").
Notation Ncompare_eq_correct := N.compare_eq_iff (compat "8.3").
Notation Nlt_irrefl := N.lt_irrefl (compat "8.3").
Notation Nlt_trans := N.lt_trans (compat "8.3").
Notation Nle_lteq := N.lt_eq_cases (compat "8.3").
Notation Nlt_succ_r := N.lt_succ_r (compat "8.3").
Notation Nle_trans := N.le_trans (compat "8.3").
Notation Nle_succ_l := N.le_succ_l (compat "8.3").
Notation Ncompare_spec := N.compare_spec (compat "8.3").
Notation Ncompare_0 := N.compare_0_r (compat "8.3").
Notation Ndouble_div2 := N.div2_double (compat "8.3").
Notation Ndouble_plus_one_div2 := N.div2_succ_double (compat "8.3").
Notation Ndouble_inj := N.double_inj (compat "8.3").
Notation Ndouble_plus_one_inj := N.succ_double_inj (compat "8.3").
Notation Npow_0_r := N.pow_0_r (compat "8.3").
Notation Npow_succ_r := N.pow_succ_r (compat "8.3").
Notation Nlog2_spec := N.log2_spec (compat "8.3").
Notation Nlog2_nonpos := N.log2_nonpos (compat "8.3").
Notation Neven_spec := N.even_spec (compat "8.3").
Notation Nodd_spec := N.odd_spec (compat "8.3").
Notation Nlt_not_eq := N.lt_neq (compat "8.3").
Notation Ngt_Nlt := N.gt_lt (compat "8.3").

More complex compatibility facts, expressed as lemmas (to preserve scopes for instance)

Lemma Nplus_reg_l n m p : n + m = n + p -> m = p.
Lemma Nmult_Sn_m n m : N.succ n * m = m + n * m.
Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m.
Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
Lemma Ncompare_antisym n m : CompOpp (n ?= m) = (m ?= n).

Definition N_ind_double a P f0 f2 fS2 := N.binary_ind P f0 f2 fS2 a.
Definition N_rec_double a P f0 f2 fS2 := N.binary_rec P f0 f2 fS2 a.

Not kept : Ncompare_n_Sm Nplus_lt_cancel_l