← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/FSets/OrderedTypeEx.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/FSets/OrderedTypeEx.v
 
1
(***********************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 
3
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
 
4
(*   \VV/  *************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the      *)
 
6
(*         *       GNU Lesser General Public License Version 2.1       *)
 
7
(***********************************************************************)
 
8
 
 
9
(* Finite sets library.  
 
10
 * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
 
11
 * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
 
12
 *              91405 Orsay, France *)
 
13
 
 
14
(* $Id: OrderedTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *)
 
15
 
 
16
Require Import OrderedType.
 
17
Require Import ZArith.
 
18
Require Import Omega.
 
19
Require Import NArith Ndec.
 
20
Require Import Compare_dec.
 
21
 
 
22
(** * Examples of Ordered Type structures. *)
 
23
 
 
24
(** First, a particular case of [OrderedType] where 
 
25
    the equality is the usual one of Coq. *)
 
26
 
 
27
Module Type UsualOrderedType.
 
28
 Parameter Inline t : Type.
 
29
 Definition eq := @eq t.
 
30
 Parameter Inline lt : t -> t -> Prop.
 
31
 Definition eq_refl := @refl_equal t.
 
32
 Definition eq_sym := @sym_eq t.
 
33
 Definition eq_trans := @trans_eq t.
 
34
 Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 
35
 Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
36
 Parameter compare : forall x y : t, Compare lt eq x y.
 
37
 Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
 
38
End UsualOrderedType.
 
39
 
 
40
(** a [UsualOrderedType] is in particular an [OrderedType]. *)
 
41
 
 
42
Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.
 
43
 
 
44
(** [nat] is an ordered type with respect to the usual order on natural numbers. *)
 
45
 
 
46
Module Nat_as_OT <: UsualOrderedType.
 
47
 
 
48
  Definition t := nat.
 
49
 
 
50
  Definition eq := @eq nat.
 
51
  Definition eq_refl := @refl_equal t.
 
52
  Definition eq_sym := @sym_eq t.
 
53
  Definition eq_trans := @trans_eq t.
 
54
 
 
55
  Definition lt := lt.
 
56
 
 
57
  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 
58
  Proof. unfold lt in |- *; intros; apply lt_trans with y; auto. Qed.
 
59
 
 
60
  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
61
  Proof. unfold lt, eq in |- *; intros; omega. Qed.
 
62
 
 
63
  Definition compare : forall x y : t, Compare lt eq x y.
 
64
  Proof.
 
65
    intros; case (lt_eq_lt_dec x y).
 
66
    simple destruct 1; intro.
 
67
    constructor 1; auto.
 
68
    constructor 2; auto.
 
69
    intro; constructor 3; auto.
 
70
  Defined.
 
71
 
 
72
  Definition eq_dec := eq_nat_dec.
 
73
 
 
74
End Nat_as_OT.
 
75
 
 
76
 
 
77
(** [Z] is an ordered type with respect to the usual order on integers. *)
 
78
 
 
79
Open Local Scope Z_scope.
 
80
 
 
81
Module Z_as_OT <: UsualOrderedType.
 
82
 
 
83
  Definition t := Z.
 
84
  Definition eq := @eq Z. 
 
85
  Definition eq_refl := @refl_equal t.
 
86
  Definition eq_sym := @sym_eq t.
 
87
  Definition eq_trans := @trans_eq t.
 
88
 
 
89
  Definition lt (x y:Z) := (x<y).
 
90
 
 
91
  Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.
 
92
  Proof. intros; omega. Qed.
 
93
 
 
94
  Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
 
95
  Proof. intros; omega. Qed.
 
96
 
 
97
  Definition compare : forall x y, Compare lt eq x y.
 
98
  Proof.
 
99
    intros x y; case_eq (x ?= y); intros.
 
100
    apply EQ; unfold eq; apply Zcompare_Eq_eq; auto.
 
101
    apply LT; unfold lt, Zlt; auto.
 
102
    apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto.
 
103
  Defined.
 
104
 
 
105
  Definition eq_dec := Z_eq_dec.
 
106
 
 
107
End Z_as_OT.
 
108
 
 
109
(** [positive] is an ordered type with respect to the usual order on natural numbers. *) 
 
110
 
 
111
Open Local Scope positive_scope.
 
112
 
 
113
Module Positive_as_OT <: UsualOrderedType.
 
114
  Definition t:=positive.
 
115
  Definition eq:=@eq positive.
 
116
  Definition eq_refl := @refl_equal t.
 
117
  Definition eq_sym := @sym_eq t.
 
118
  Definition eq_trans := @trans_eq t.
 
119
 
 
120
  Definition lt p q:= (p ?= q) Eq = Lt.
 
121
 
 
122
  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 
123
  Proof. 
 
124
  unfold lt; intros x y z.
 
125
  change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z).
 
126
  omega.
 
127
  Qed.
 
128
 
 
129
  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
130
  Proof.
 
131
  intros; intro.
 
132
  rewrite H0 in H.
 
133
  unfold lt in H.
 
134
  rewrite Pcompare_refl in H; discriminate.
 
135
  Qed.
 
136
 
 
137
  Definition compare : forall x y : t, Compare lt eq x y.
 
138
  Proof.
 
139
  intros x y.
 
140
  case_eq ((x ?= y) Eq); intros.
 
141
  apply EQ; apply Pcompare_Eq_eq; auto.
 
142
  apply LT; unfold lt; auto.
 
143
  apply GT; unfold lt.
 
144
  replace Eq with (CompOpp Eq); auto.
 
145
  rewrite <- Pcompare_antisym; rewrite H; auto.
 
146
  Defined.
 
147
 
 
148
  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
149
  Proof.
 
150
   intros; unfold eq; decide equality.
 
151
  Defined.
 
152
 
 
153
End Positive_as_OT.
 
154
 
 
155
 
 
156
(** [N] is an ordered type with respect to the usual order on natural numbers. *) 
 
157
 
 
158
Open Local Scope positive_scope.
 
159
 
 
160
Module N_as_OT <: UsualOrderedType.
 
161
  Definition t:=N.
 
162
  Definition eq:=@eq N.
 
163
  Definition eq_refl := @refl_equal t.
 
164
  Definition eq_sym := @sym_eq t.
 
165
  Definition eq_trans := @trans_eq t.
 
166
 
 
167
  Definition lt p q:= Nleb q p = false.
 
168
 
 
169
  Definition lt_trans := Nltb_trans.
 
170
 
 
171
  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
172
  Proof.
 
173
  intros; intro.
 
174
  rewrite H0 in H.
 
175
  unfold lt in H.
 
176
  rewrite Nleb_refl in H; discriminate.
 
177
  Qed.
 
178
 
 
179
  Definition compare : forall x y : t, Compare lt eq x y.
 
180
  Proof.
 
181
  intros x y.
 
182
  case_eq ((x ?= y)%N); intros.
 
183
  apply EQ; apply Ncompare_Eq_eq; auto.
 
184
  apply LT; unfold lt; auto.
 
185
   generalize (Nleb_Nle y x).
 
186
   unfold Nle; rewrite <- Ncompare_antisym.
 
187
   destruct (x ?= y)%N; simpl; try discriminate.
 
188
   clear H; intros H.
 
189
   destruct (Nleb y x); intuition.
 
190
  apply GT; unfold lt.
 
191
   generalize (Nleb_Nle x y).
 
192
   unfold Nle; destruct (x ?= y)%N; simpl; try discriminate.
 
193
   destruct (Nleb x y); intuition.
 
194
  Defined.
 
195
 
 
196
  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
197
  Proof.
 
198
   intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
 
199
  Defined.
 
200
 
 
201
End N_as_OT.
 
202
 
 
203
 
 
204
(** From two ordered types, we can build a new OrderedType 
 
205
   over their cartesian product, using the lexicographic order. *)
 
206
 
 
207
Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 
208
 Module MO1:=OrderedTypeFacts(O1).
 
209
 Module MO2:=OrderedTypeFacts(O2).
 
210
 
 
211
 Definition t := prod O1.t O2.t.
 
212
  
 
213
 Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y).
 
214
 
 
215
 Definition lt x y := 
 
216
    O1.lt (fst x) (fst y) \/ 
 
217
    (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).
 
218
 
 
219
 Lemma eq_refl : forall x : t, eq x x.
 
220
 Proof. 
 
221
 intros (x1,x2); red; simpl; auto.
 
222
 Qed.
 
223
 
 
224
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
 
225
 Proof. 
 
226
 intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
 
227
 Qed.
 
228
 
 
229
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
 
230
 Proof. 
 
231
 intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
 
232
 Qed.
 
233
 
 
234
 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. 
 
235
 Proof.
 
236
 intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition.
 
237
 left; eauto.
 
238
 left; eapply MO1.lt_eq; eauto.
 
239
 left; eapply MO1.eq_lt; eauto.
 
240
 right; split; eauto.
 
241
 Qed.
 
242
 
 
243
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
244
 Proof.
 
245
 intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition.
 
246
 apply (O1.lt_not_eq H0 H1).
 
247
 apply (O2.lt_not_eq H3 H2).
 
248
 Qed.
 
249
 
 
250
 Definition compare : forall x y : t, Compare lt eq x y.
 
251
 intros (x1,x2) (y1,y2).
 
252
 destruct (O1.compare x1 y1).
 
253
 apply LT; unfold lt; auto.
 
254
 destruct (O2.compare x2 y2).
 
255
 apply LT; unfold lt; auto.
 
256
 apply EQ; unfold eq; auto.
 
257
 apply GT; unfold lt; auto.
 
258
 apply GT; unfold lt; auto.
 
259
 Defined.
 
260
 
 
261
 Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
 
262
 Proof.
 
263
 intros; elim (compare x y); intro H; [ right | left | right ]; auto.
 
264
 auto using lt_not_eq.
 
265
 assert (~ eq y x); auto using lt_not_eq, eq_sym.
 
266
 Defined.
 
267
 
 
268
End PairOrderedType.
 
269