blob: 0531bd0a16295c18265f4d5b7c889024084e6b0c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
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}.
Proof.
intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
intuition eauto.
Qed.
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.
Proof.
intros; unfold Reqb; destruct Req_dec as [EQ|NEQ]; auto with *.
split; try discriminate. intro EQ; elim NEQ; auto.
Qed.
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).
Proof.
intros. unfold Rcompare.
destruct total_order_T as [[H|H]|H]; auto.
Qed.
Module R_as_OT <: OrderedTypeFull.
Include R_as_DT.
Definition lt := Rlt.
Definition le := Rle.
Definition compare := Rcompare.
Instance lt_strorder : StrictOrder Rlt.
Proof. split; [ exact Rlt_irrefl | exact Rlt_trans ]. Qed.
Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Rlt.
Proof. repeat red; intros; subst; auto. Qed.
Lemma le_lteq : forall x y, x <= y <-> x < y \/ x = y.
Proof. unfold Rle; auto with *. Qed.
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]. *)
|
