Library Coq.Reals.ROrderedType
Require
Import
Rbase
Equalities
Orders
OrdersTac
.
Local Open
Scope
R_scope
.
DecidableType structure for real numbers
Lemma
Req_dec
:
forall
r1
r2
:
R
,
{
r1
=
r2
}
+
{
r1
<>
r2
}
.
Definition
Reqb
r1
r2
:=
if
Req_dec
r1
r2
then
true
else
false
.
Lemma
Reqb_eq
:
forall
r1
r2
,
Reqb
r1
r2
=
true
<->
r1
=
r2
.
Module
R_as_UBE
<:
UsualBoolEq
.
Definition
t
:=
R
.
Definition
eq
:= @
eq
R
.
Definition
eqb
:=
Reqb
.
Definition
eqb_eq
:=
Reqb_eq
.
End
R_as_UBE
.
Module
R_as_DT
<:
UsualDecidableTypeFull
:=
Make_UDTF
R_as_UBE
.
Note that the last module fulfills by subtyping many other interfaces, such as
DecidableType
or
EqualityType
.
Note that
R_as_DT
can also be seen as a
DecidableType
and a
DecidableTypeOrig
.
OrderedType structure for binary integers
Definition
Rcompare
x
y
:=
match
total_order_T
x
y
with
|
inleft
(
left
_
) =>
Lt
|
inleft
(
right
_
) =>
Eq
|
inright
_
=>
Gt
end
.
Lemma
Rcompare_spec
:
forall
x
y
,
CompareSpec
(
x
=
y
) (
x
<
y
) (
y
<
x
) (
Rcompare
x
y
).
Module
R_as_OT
<:
OrderedTypeFull
.
Include
R_as_DT
.
Definition
lt
:=
Rlt
.
Definition
le
:=
Rle
.
Definition
compare
:=
Rcompare
.
Instance
lt_strorder
:
StrictOrder
Rlt
.
Instance
lt_compat
:
Proper
(
Logic.eq
==>
Logic.eq
==>
iff
)
Rlt
.
Lemma
le_lteq
:
forall
x
y
,
x
<=
y
<->
x
<
y
\/
x
=
y
.
Definition
compare_spec
:=
Rcompare_spec
.
End
R_as_OT
.
Note that
R_as_OT
can also be seen as a
UsualOrderedType
and a
OrderedType
(and also as a
DecidableType
).
An
order
tactic for real numbers
Module
ROrder
:=
OTF_to_OrderTac
R_as_OT
.
Ltac
r_order
:=
ROrder.order
.
Note that
r_order
is domain-agnostic: it will not prove
1<=2
or
x
<=
x
+
x
, but rather things like
x
<=
y
->
y
<=
x
->
x
=
y
.