Library Coq.Bool.BoolOrder
The order relations
le
lt
and
compare
are defined in
Bool.v
Order properties of
bool
Require
Export
Bool
.
Require
Import
Orders
.
Import
BoolNotations
.
Order
le
Lemma
le_refl
:
forall
b
,
b
<=
b
.
Lemma
le_trans
:
forall
b1
b2
b3
,
b1
<=
b2
->
b2
<=
b3
->
b1
<=
b3
.
Lemma
le_true
:
forall
b
,
b
<=
true
.
Lemma
false_le
:
forall
b
,
false
<=
b
.
Instance
le_compat
:
Proper
(
eq
==>
eq
==>
iff
)
Bool.le
.
Strict order
lt
Lemma
lt_irrefl
:
forall
b
,
~
b
<
b
.
Lemma
lt_trans
:
forall
b1
b2
b3
,
b1
<
b2
->
b2
<
b3
->
b1
<
b3
.
Instance
lt_compat
:
Proper
(
eq
==>
eq
==>
iff
)
Bool.lt
.
Lemma
lt_trichotomy
:
forall
b1
b2
,
{
b1
<
b2
}
+
{
b1
=
b2
}
+
{
b2
<
b1
}
.
Lemma
lt_total
:
forall
b1
b2
,
b1
<
b2
\/
b1
=
b2
\/
b2
<
b1
.
Lemma
lt_le_incl
:
forall
b1
b2
,
b1
<
b2
->
b1
<=
b2
.
Lemma
le_lteq_dec
:
forall
b1
b2
,
b1
<=
b2
->
{
b1
<
b2
}
+
{
b1
=
b2
}
.
Lemma
le_lteq
:
forall
b1
b2
,
b1
<=
b2
<->
b1
<
b2
\/
b1
=
b2
.
Order structures
Instance
le_preorder
:
PreOrder
Bool.le
.
Instance
lt_strorder
:
StrictOrder
Bool.lt
.
Module
BoolOrd
<:
UsualDecidableTypeFull
<:
OrderedTypeFull
<:
TotalOrder
.
Definition
t
:=
bool
.
Definition
eq
:= @
eq
bool
.
Definition
eq_equiv
:= @
eq_equivalence
bool
.
Definition
lt
:=
Bool.lt
.
Definition
lt_strorder
:=
lt_strorder
.
Definition
lt_compat
:=
lt_compat
.
Definition
le
:=
Bool.le
.
Definition
le_lteq
:=
le_lteq
.
Definition
lt_total
:=
lt_total
.
Definition
compare
:=
Bool.compare
.
Definition
compare_spec
:=
compare_spec
.
Definition
eq_dec
:=
bool_dec
.
Definition
eq_refl
:= @
eq_Reflexive
bool
.
Definition
eq_sym
:= @
eq_Symmetric
bool
.
Definition
eq_trans
:= @
eq_Transitive
bool
.
Definition
eqb
:=
eqb
.
Definition
eqb_eq
:=
eqb_true_iff
.
End
BoolOrd
.