Library Coq.NArith.Ndec



Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import BinPos.
Require Import BinNat.
Require Import Pnat.
Require Import Nnat.
Require Import Ndigits.

A boolean equality over N

Fixpoint Peqb (p1 p2:positive) {struct p2} : bool :=
  match p1, p2 with
  | xH, xH => true
  | xO p'1, xO p'2 => Peqb p'1 p'2
  | xI p'1, xI p'2 => Peqb p'1 p'2
  | _, _ => false
  end.

Lemma Peqb_correct : forall p, Peqb p p = true.

Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq.

Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.

Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true.

Definition Neqb (a a':N) :=
  match a, a' with
  | N0, N0 => true
  | Npos p, Npos p' => Peqb p p'
  | _, _ => false
  end.

Lemma Neqb_correct : forall n, Neqb n n = true.

Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq.

Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true.

Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'.

Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a.

Lemma Nxor_eq_true :
 forall a a', Nxor a a' = N0 -> Neqb a a' = true.


Lemma Nxor_eq_false :
 forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false.



Lemma Nodd_not_double :
 forall a,
   Nodd a -> forall a0, Neqb (Ndouble a0) a = false.



Lemma Nnot_div2_not_double :
 forall a a0,
   Neqb (Ndiv2 a) a0 = false -> Neqb a (Ndouble a0) = false.





Lemma Neven_not_double_plus_one :
 forall a,
   Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false.


Lemma Nnot_div2_not_double_plus_one :
 forall a a0,
   Neqb (Ndiv2 a) a0 = false -> Neqb (Ndouble_plus_one a0) a = false.





Lemma Nbit0_neq :
 forall a a',
   Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false.



Lemma Ndiv2_eq :
 forall a a', Neqb a a' = true -> Neqb (Ndiv2 a) (Ndiv2 a') = true.



Lemma Ndiv2_neq :
 forall a a',
   Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false.



Lemma Ndiv2_bit_eq :
 forall a a',
   Nbit0 a = Nbit0 a' -> Ndiv2 a = Ndiv2 a' -> a = a'.





Lemma Ndiv2_bit_neq :
 forall a a',
   Neqb a a' = false ->
   Nbit0 a = Nbit0 a' -> Neqb (Ndiv2 a) (Ndiv2 a') = false.



Lemma Nneq_elim :
 forall a a',
   Neqb a a' = false ->
   Nbit0 a = negb (Nbit0 a') \/
   Neqb (Ndiv2 a) (Ndiv2 a') = false.




Lemma Ndouble_or_double_plus_un :
 forall a,
   {a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}.




A boolean order on N

Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b).

Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b.

Lemma Nleb_refl : forall a, Nleb a a = true.


Lemma Nleb_antisym :
 forall a b, Nleb a b = true -> Nleb b a = true -> a = b.



Lemma Nleb_trans :
 forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true.




Lemma Nleb_ltb_trans :
 forall a b c,
   Nleb a b = true -> Nleb c b = false -> Nleb c a = false.




Lemma Nltb_leb_trans :
 forall a b c,
   Nleb b a = false -> Nleb b c = true -> Nleb c a = false.




Lemma Nltb_trans :
 forall a b c,
   Nleb b a = false -> Nleb c b = false -> Nleb c a = false.




Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true.



Lemma Nleb_double_mono :
 forall a b,
   Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true.




Lemma Nleb_double_plus_one_mono :
 forall a b,
   Nleb a b = true ->
   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true.




Lemma Nleb_double_mono_conv :
 forall a b,
   Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true.



Lemma Nleb_double_plus_one_mono_conv :
 forall a b,
   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true ->
   Nleb a b = true.



Lemma Nltb_double_mono :
 forall a b,
   Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false.



Lemma Nltb_double_plus_one_mono :
 forall a b,
   Nleb a b = false ->
   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false.



Lemma Nltb_double_mono_conv :
 forall a b,
   Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false.


Lemma Nltb_double_plus_one_mono_conv :
 forall a b,
   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false ->
   Nleb a b = false.




Definition Nmin' (a b:N) := if Nleb a b then a else b.

Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b.

Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}.

Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true.



Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true.



Lemma Nmin_le_3 :
 forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true.



Lemma Nmin_le_4 :
 forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true.



Lemma Nmin_le_5 :
 forall a b c,
   Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true.



Lemma Nmin_lt_3 :
 forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false.



Lemma Nmin_lt_4 :
 forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false.