← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/FSets/OrderedTypeAlt.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/OrderedTypeAlt.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: OrderedTypeAlt.v 11699 2008-12-18 11:49:08Z letouzey $ *)
 
15
 
 
16
Require Import OrderedType.
 
17
 
 
18
(** * An alternative (but equivalent) presentation for an Ordered Type
 
19
   inferface. *)
 
20
 
 
21
(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
 
22
whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ] 
 
23
*)
 
24
 
 
25
Module Type OrderedTypeAlt.
 
26
 
 
27
 Parameter t : Type.
 
28
 
 
29
 Parameter compare : t -> t -> comparison.
 
30
 
 
31
 Infix "?=" := compare (at level 70, no associativity).
 
32
 
 
33
 Parameter compare_sym : 
 
34
   forall x y, (y?=x) = CompOpp (x?=y).
 
35
 Parameter compare_trans : 
 
36
   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
 
37
 
 
38
End OrderedTypeAlt. 
 
39
 
 
40
(** From this new presentation to the original one. *)
 
41
 
 
42
Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
 
43
 Import O.
 
44
 
 
45
 Definition t := t.
 
46
 
 
47
 Definition eq x y := (x?=y) = Eq.
 
48
 Definition lt x y := (x?=y) = Lt.
 
49
 
 
50
 Lemma eq_refl : forall x, eq x x.
 
51
 Proof.
 
52
 intro x.
 
53
 unfold eq.
 
54
 assert (H:=compare_sym x x).
 
55
 destruct (x ?= x); simpl in *; try discriminate; auto.
 
56
 Qed.
 
57
 
 
58
 Lemma eq_sym : forall x y, eq x y -> eq y x.
 
59
 Proof. 
 
60
 unfold eq; intros.
 
61
 rewrite compare_sym.
 
62
 rewrite H; simpl; auto.
 
63
 Qed.
 
64
 
 
65
 Definition eq_trans := (compare_trans Eq).
 
66
 
 
67
 Definition lt_trans := (compare_trans Lt).
 
68
 
 
69
 Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
 
70
 Proof.
 
71
 unfold eq, lt; intros.
 
72
 rewrite H; discriminate.
 
73
 Qed.
 
74
 
 
75
 Definition compare : forall x y, Compare lt eq x y.
 
76
 Proof.
 
77
 intros.
 
78
 case_eq (x ?= y); intros.
 
79
 apply EQ; auto.
 
80
 apply LT; auto.
 
81
 apply GT; red.
 
82
 rewrite compare_sym; rewrite H; auto.
 
83
 Defined.
 
84
 
 
85
 Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
86
 Proof.
 
87
 intros; unfold eq.
 
88
 case (x ?= y); [ left | right | right ]; auto; discriminate.
 
89
 Defined.
 
90
 
 
91
End OrderedType_from_Alt. 
 
92
 
 
93
(** From the original presentation to this alternative one. *)
 
94
 
 
95
Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
 
96
 Import O.
 
97
 Module MO:=OrderedTypeFacts(O).
 
98
 Import MO.
 
99
 
 
100
 Definition t := t.
 
101
 
 
102
 Definition compare x y := match compare x y with 
 
103
   | LT _ => Lt
 
104
   | EQ _ => Eq
 
105
   | GT _ => Gt
 
106
  end. 
 
107
 
 
108
 Infix "?=" := compare (at level 70, no associativity).
 
109
 
 
110
 Lemma compare_sym : 
 
111
   forall x y, (y?=x) = CompOpp (x?=y).
 
112
 Proof.
 
113
 intros x y; unfold compare.
 
114
 destruct O.compare; elim_comp; simpl; auto.
 
115
 Qed.
 
116
 
 
117
 Lemma compare_trans : 
 
118
   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
 
119
 Proof.
 
120
 intros c x y z.
 
121
 destruct c; unfold compare; 
 
122
 do 2 (destruct O.compare; intros; try discriminate); 
 
123
 elim_comp; auto.
 
124
 Qed.
 
125
 
 
126
End OrderedType_to_Alt.
 
127
 
 
128