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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
Require Import Basics OrdersTac.
Require Export Orders.
Set Implicit Arguments.
Unset Strict Implicit.
(** * Properties of [OrderedTypeFull] *)
Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
Module OrderTac := OTF_to_OrderTac O.
Ltac order := OrderTac.order.
Ltac iorder := intuition order.
Instance le_compat : Proper (eq==>eq==>iff) le.
Proof. repeat red; iorder. Qed.
Instance le_preorder : PreOrder le.
Proof. split; red; order. Qed.
Instance le_order : PartialOrder eq le.
Proof. compute; iorder. Qed.
Instance le_antisym : Antisymmetric _ eq le.
Proof. apply partial_order_antisym; auto with *. Qed.
Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
Proof. iorder. Qed.
Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
Proof. iorder. Qed.
Lemma le_or_gt : forall x y, x<=y \/ y<x.
Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
Lemma lt_or_ge : forall x y, x<y \/ y<=x.
Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
Proof. iorder. Qed.
End OrderedTypeFullFacts.
(** * Properties of [OrderedType] *)
Module OrderedTypeFacts (Import O: OrderedType').
Module OrderTac := OT_to_OrderTac O.
Ltac order := OrderTac.order.
Notation "x <= y" := (~lt y x) : order.
Infix "?=" := compare (at level 70, no associativity) : order.
Local Open Scope order.
Tactic Notation "elim_compare" constr(x) constr(y) :=
destruct (compare_spec x y).
Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
destruct (compare_spec x y) as [h|h|h].
(** The following lemmas are either re-phrasing of [eq_equiv] and
[lt_strorder] or immediately provable by [order]. Interest:
compatibility, test of order, etc *)
Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
Equivalence_Transitive x y z.
Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
StrictOrder_Transitive x y z.
Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
(** Some more about [compare] *)
Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
Proof.
intros; elim_compare x y; intuition; try discriminate; order.
Qed.
Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
Proof.
intros; elim_compare x y; intuition; try discriminate; order.
Qed.
Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
Proof.
intros; elim_compare x y; intuition; try discriminate; order.
Qed.
Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
Proof.
intros; rewrite compare_lt_iff; intuition.
Qed.
Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
Proof.
intros; rewrite compare_gt_iff; intuition.
Qed.
Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
Proof.
intros x x' Hxx' y y' Hyy'.
elim_compare x' y'; autorewrite with order; order.
Qed.
Lemma compare_refl : forall x, (x ?= x) = Eq.
Proof.
intros; elim_compare x x; auto; order.
Qed.
Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
Proof.
intros; elim_compare x y; simpl; autorewrite with order; order.
Qed.
(** For compatibility reasons *)
Definition eq_dec := eq_dec.
Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
Proof.
intros x y; destruct (CompSpec2Type (compare_spec x y));
[ right | left | right ]; order.
Defined.
Definition eqb x y : bool := if eq_dec x y then true else false.
Lemma if_eq_dec : forall x y (B:Type)(b b':B),
(if eq_dec x y then b else b') =
(match compare x y with Eq => b | _ => b' end).
Proof.
intros; destruct eq_dec; elim_compare x y; auto; order.
Qed.
Lemma eqb_alt :
forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
Proof.
unfold eqb; intros; apply if_eq_dec.
Qed.
Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
Proof.
intros x x' Hxx' y y' Hyy'.
rewrite 2 eqb_alt, Hxx', Hyy'; auto.
Qed.
End OrderedTypeFacts.
(** * Tests of the order tactic
Is it at least capable of proving some basic properties ? *)
Module OrderedTypeTest (Import O:OrderedType').
Module Import MO := OrderedTypeFacts O.
Local Open Scope order.
Lemma lt_not_eq x y : x<y -> ~x==y. Proof. order. Qed.
Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.
Proof. intuition; order. Qed.
End OrderedTypeTest.
(** * Reversed OrderedTypeFull.
we can switch the orientation of the order. This is used for
example when deriving properties of [min] out of the ones of [max]
(see [GenericMinMax]).
*)
Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
Definition t := O.t.
Definition eq := O.eq.
Program Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.
Definition lt := flip O.lt.
Definition le := flip O.le.
Instance lt_strorder: StrictOrder lt.
Proof. unfold lt; auto with *. Qed.
Instance lt_compat : Proper (eq==>eq==>iff) lt.
Proof. unfold lt; auto with *. Qed.
Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
Definition compare := flip O.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof.
intros; unfold compare, eq, lt, flip.
destruct (O.compare_spec y x); auto with relations.
Qed.
End OrderedTypeRev.
|
