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.

#[global]
 Instance lt_strorder : StrictOrder Rlt.

#[global]
 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.