# 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.