Library Coq.NArith.Ndec
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.