# Library Coq.NArith.BinNat

Require Import BinPos.
Binary natural numbers
Inductive N : Set :=
| N0 : N
| Npos : positive -> N.
Declare binding key for scope positive_scope
Delimit Scope N_scope with N.
Automatically open scope positive_scope for the constructors of N
Open Local Scope N_scope.
Definition Ndiscr : forall n:N, { p : positive | n = Npos p } + { n = N0 }.
Operation x -> 2*x+1
Definition Ndouble_plus_one x :=
match x with
| N0 => Npos 1
| Npos p => Npos (xI p)
end.
Operation x -> 2*x
Definition Ndouble n :=
match n with
| N0 => N0
| Npos p => Npos (xO p)
end.
Successor
Definition Nsucc n :=
match n with
| N0 => Npos 1
| Npos p => Npos (Psucc p)
end.
Predecessor
Definition Npred (n : N) := match n with
| N0 => N0
| Npos p => match p with
| xH => N0
| _ => Npos (Ppred p)
end
end.
Addition
Definition Nplus n m :=
match n, m with
| N0, _ => m
| _, N0 => n
| Npos p, Npos q => Npos (p + q)
end.
Infix "+" := Nplus : N_scope.
Subtraction
Definition Nminus (n m : N) :=
match n, m with
| N0, _ => N0
| n, N0 => n
| Npos n', Npos m' =>
match Pminus_mask n' m' with
| IsPos p => Npos p
| _ => N0
end
end.
Infix "-" := Nminus : N_scope.
Multiplication
Definition Nmult n m :=
match n, m with
| N0, _ => N0
| _, N0 => N0
| Npos p, Npos q => Npos (p * q)
end.
Infix "*" := Nmult : N_scope.
Boolean Equality
Definition Neqb n m :=
match n, m with
| N0, N0 => true
| Npos n, Npos m => Peqb n m
| _,_ => false
end.
Order
Definition Ncompare n m :=
match n, m with
| N0, N0 => Eq
| N0, Npos m' => Lt
| Npos n', N0 => Gt
| Npos n', Npos m' => (n' ?= m')%positive Eq
end.
Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
Definition Nlt (x y:N) := ( x ?= y ) = Lt.
Definition Ngt (x y:N) := ( x ?= y ) = Gt.
Definition Nle (x y:N) := ( x ?= y ) <> Gt.
Definition Nge (x y:N) := ( x ?= y ) <> Lt.
Infix "<=" := Nle : N_scope.
Infix "<" := Nlt : N_scope.
Infix ">=" := Nge : N_scope.
Infix ">" := Ngt : N_scope.
Min and max
Definition Nmin (n n' : N) := match Ncompare n n' with
| Lt | Eq => n
| Gt => n'
end.
Definition Nmax (n n' : N) := match Ncompare n n' with
| Lt | Eq => n'
| Gt => n
end.
Decidability of equality.
Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }.
convenient induction principles
Lemma N_ind_double :
forall (a:N) (P:N -> Prop),
P N0 ->
(forall a, P a -> P (Ndouble a)) ->
(forall a, P a -> P (Ndouble_plus_one a)) -> P a.
Lemma N_rec_double :
forall (a:N) (P:N -> Set),
P N0 ->
(forall a, P a -> P (Ndouble a)) ->
(forall a, P a -> P (Ndouble_plus_one a)) -> P a.
Peano induction on binary natural numbers
Definition Nrect
(P : N -> Type) (a : P N0)
(f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n :=
let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
let P' (p : positive) := P (Npos p) in
match n return (P n) with
| N0 => a
| Npos p => Prect P' (f N0 a) f' p
end.
Theorem Nrect_base : forall P a f, Nrect P a f N0 = a.
Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n).
Definition Nind (P : N -> Prop) := Nrect P.
Definition Nrec (P : N -> Set) := Nrect P.
Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
Properties of successor and predecessor
Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n.
Properties of addition
Theorem Nplus_0_l : forall n:N, N0 + n = n.
Theorem Nplus_0_r : forall n:N, n + N0 = n.
Theorem Nplus_comm : forall n m:N, n + m = m + n.
Theorem Nplus_assoc : forall n m p:N, n + ( m + p ) = n + m + p.
Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m).
Theorem Nsucc_0 : forall n : N, Nsucc n <> N0.
Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p.
Properties of subtraction.
Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'.
Theorem Nminus_0_r : forall n : N, n - N0 = n.
Theorem Nminus_succ_r : forall n m : N, n - ( Nsucc m ) = Npred (n - m).
Properties of multiplication
Theorem Nmult_0_l : forall n:N, N0 * n = N0.
Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
Theorem Nmult_Sn_m : forall n m : N, ( Nsucc n ) * m = m + n * m.
Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
Theorem Nmult_comm : forall n m:N, n * m = m * n.
Theorem Nmult_assoc : forall n m p:N, n * ( m * p ) = n * m * p.
Theorem Nmult_plus_distr_r : forall n m p:N, ( n + m ) * p = n * p + m * p.
Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
Properties of boolean order.
Lemma Neqb_eq : forall n m, Neqb n m = true <-> n = m.
Properties of comparison
Lemma Ncompare_refl : forall n, ( n ?= n ) = Eq.
Theorem Ncompare_Eq_eq : forall n m:N, ( n ?= m ) = Eq -> n = m.
Theorem Ncompare_eq_correct : forall n m:N, ( n ?= m ) = Eq <-> n = m.
Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = ( m ?= n ).
Lemma Ngt_Nlt : forall n m, n > m -> m < n.
Theorem Nlt_irrefl : forall n : N, ~ n < n.
Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q.
Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m.
Theorem Ncompare_n_Sm :
forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x = y.
Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y).
0 is the least natural number
Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
Dividing by 2
Definition Ndiv2 (n:N) :=
match n with
| N0 => N0
| Npos 1 => N0
| Npos (xO p) => Npos p
| Npos (xI p) => Npos p
end.
Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n.
Lemma Ndouble_plus_one_div2 :
forall n:N, Ndiv2 (Ndouble_plus_one n) = n.
Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m.
Lemma Ndouble_plus_one_inj :
forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m.