Library Coq.ZArith.ZArith_dec
Require
Import
Sumbool
.
Require
Import
BinInt
.
Require
Import
Zorder
.
Require
Import
Zcompare
.
Open
Local
Scope
Z_scope
.
Lemma
Dcompare_inf
:
forall
r
:comparison, {
r
=
Eq
} + {
r
=
Lt
} + {
r
=
Gt
}.
Lemma
Zcompare_rec
:
forall
(
P
:Set) (
n
m
:Z),
((
n
?=
m
) =
Eq
->
P
) -> ((
n
?=
m
) =
Lt
->
P
) -> ((
n
?=
m
) =
Gt
->
P
) ->
P
.
Section
decidability
.
Variables
x
y
:
Z
.
Decidability of equality on binary integers
Definition
Z_eq_dec
: {
x
=
y
} + {
x
<>
y
}.
Decidability of order on binary integers
Definition
Z_lt_dec
: {
x
<
y
} + {~
x
<
y
}.
Definition
Z_le_dec
: {
x
<=
y
} + {~
x
<=
y
}.
Definition
Z_gt_dec
: {
x
>
y
} + {~
x
>
y
}.
Definition
Z_ge_dec
: {
x
>=
y
} + {~
x
>=
y
}.
Definition
Z_lt_ge_dec
: {
x
<
y
} + {
x
>=
y
}.
Lemma
Z_lt_le_dec
: {
x
<
y
} + {
y
<=
x
}.
Definition
Z_le_gt_dec
: {
x
<=
y
} + {
x
>
y
}.
Definition
Z_gt_le_dec
: {
x
>
y
} + {
x
<=
y
}.
Definition
Z_ge_lt_dec
: {
x
>=
y
} + {
x
<
y
}.
Definition
Z_le_lt_eq_dec
:
x
<=
y
-> {
x
<
y
} + {
x
=
y
}.
End
decidability
.
Cotransitivity of order on binary integers
Lemma
Zlt_cotrans
:
forall
n
m
:Z,
n
<
m
->
forall
p
:Z, {
n
<
p
} + {
p
<
m
}.
Lemma
Zlt_cotrans_pos
:
forall
n
m
:Z, 0 <
n
+
m
-> {0 <
n
} + {0 <
m
}.
Lemma
Zlt_cotrans_neg
:
forall
n
m
:Z,
n
+
m
< 0 -> {
n
< 0} + {
m
< 0}.
Lemma
not_Zeq_inf
:
forall
n
m
:Z,
n
<>
m
-> {
n
<
m
} + {
m
<
n
}.
Lemma
Z_dec
:
forall
n
m
:Z, {
n
<
m
} + {
n
>
m
} + {
n
=
m
}.
Lemma
Z_dec'
:
forall
n
m
:Z, {
n
<
m
} + {
m
<
n
} + {
n
=
m
}.
Definition
Z_zerop
:
forall
x
:Z, {
x
= 0} + {
x
<> 0}.
Definition
Z_notzerop
(
x
:Z) :=
sumbool_not
_
_
(
Z_zerop
x
).
Definition
Z_noteq_dec
(
x
y
:Z) :=
sumbool_not
_
_
(
Z_eq_dec
x
y
).