← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Sets/Uniset.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/Sets/Uniset.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Uniset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
10
 
 
11
(** Sets as characteristic functions *)
 
12
 
 
13
(* G. Huet 1-9-95 *)
 
14
(* Updated Papageno 12/98 *)
 
15
 
 
16
Require Import Bool.
 
17
 
 
18
Set Implicit Arguments.
 
19
 
 
20
Section defs.
 
21
 
 
22
Variable A : Set.
 
23
Variable eqA : A -> A -> Prop.
 
24
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
25
 
 
26
Inductive uniset : Set :=
 
27
    Charac : (A -> bool) -> uniset.
 
28
 
 
29
Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a.
 
30
 
 
31
Definition Emptyset := Charac (fun a:A => false).
 
32
 
 
33
Definition Fullset := Charac (fun a:A => true).
 
34
 
 
35
Definition Singleton (a:A) :=
 
36
  Charac
 
37
    (fun a':A =>
 
38
       match eqA_dec a a' with
 
39
       | left h => true
 
40
       | right h => false
 
41
       end).
 
42
 
 
43
Definition In (s:uniset) (a:A) : Prop := charac s a = true.
 
44
Hint Unfold In.
 
45
 
 
46
(** uniset inclusion *)
 
47
Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).
 
48
Hint Unfold incl.
 
49
 
 
50
(** uniset equality *)
 
51
Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
 
52
Hint Unfold seq.
 
53
 
 
54
Lemma leb_refl : forall b:bool, leb b b.
 
55
Proof.
 
56
destruct b; simpl in |- *; auto.
 
57
Qed.
 
58
Hint Resolve leb_refl.
 
59
 
 
60
Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 
61
Proof.
 
62
unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
 
63
Qed.
 
64
 
 
65
Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.
 
66
Proof.
 
67
unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
 
68
Qed.
 
69
 
 
70
Lemma seq_refl : forall x:uniset, seq x x.
 
71
Proof.
 
72
destruct x; unfold seq in |- *; auto.
 
73
Qed.
 
74
Hint Resolve seq_refl.
 
75
 
 
76
Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
 
77
Proof.
 
78
unfold seq in |- *.
 
79
destruct x; destruct y; destruct z; simpl in |- *; intros.
 
80
rewrite H; auto.
 
81
Qed.
 
82
 
 
83
Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.
 
84
Proof.
 
85
unfold seq in |- *.
 
86
destruct x; destruct y; simpl in |- *; auto.
 
87
Qed.
 
88
 
 
89
(** uniset union *)
 
90
Definition union (m1 m2:uniset) :=
 
91
  Charac (fun a:A => orb (charac m1 a) (charac m2 a)).
 
92
 
 
93
Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).  
 
94
Proof.  
 
95
unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.  
 
96
Qed. 
 
97
Hint Resolve union_empty_left.
 
98
 
 
99
Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
 
100
Proof.
 
101
unfold seq in |- *; unfold union in |- *; simpl in |- *.
 
102
intros x a; rewrite (orb_b_false (charac x a)); auto.
 
103
Qed.
 
104
Hint Resolve union_empty_right.
 
105
 
 
106
Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
 
107
Proof.
 
108
unfold seq in |- *; unfold charac in |- *; unfold union in |- *.
 
109
destruct x; destruct y; auto with bool.
 
110
Qed.
 
111
Hint Resolve union_comm.
 
112
 
 
113
Lemma union_ass :
 
114
 forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
 
115
Proof.
 
116
unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
 
117
destruct x; destruct y; destruct z; auto with bool.
 
118
Qed.
 
119
Hint Resolve union_ass.
 
120
 
 
121
Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
 
122
Proof.
 
123
unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
 
124
destruct x; destruct y; destruct z.
 
125
intros; elim H; auto.
 
126
Qed.
 
127
Hint Resolve seq_left.
 
128
 
 
129
Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
 
130
Proof.
 
131
unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
 
132
destruct x; destruct y; destruct z.
 
133
intros; elim H; auto.
 
134
Qed.
 
135
Hint Resolve seq_right.
 
136
 
 
137
 
 
138
(** All the proofs that follow duplicate [Multiset_of_A] *)
 
139
 
 
140
(** Here we should make uniset an abstract datatype, by hiding [Charac],
 
141
    [union], [charac]; all further properties are proved abstractly *)
 
142
 
 
143
Require Import Permut.
 
144
 
 
145
Lemma union_rotate :
 
146
 forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
 
147
Proof.
 
148
intros; apply (op_rotate uniset union seq); auto.
 
149
exact seq_trans.
 
150
Qed.
 
151
 
 
152
Lemma seq_congr :
 
153
 forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t).
 
154
Proof.
 
155
intros; apply (cong_congr uniset union seq); auto.
 
156
exact seq_trans.
 
157
Qed.
 
158
 
 
159
Lemma union_perm_left :
 
160
 forall x y z:uniset, seq (union x (union y z)) (union y (union x z)).
 
161
Proof.
 
162
intros; apply (perm_left uniset union seq); auto.
 
163
exact seq_trans.
 
164
Qed.
 
165
 
 
166
Lemma uniset_twist1 :
 
167
 forall x y z t:uniset,
 
168
   seq (union x (union (union y z) t)) (union (union y (union x t)) z).
 
169
Proof.
 
170
intros; apply (twist uniset union seq); auto.
 
171
exact seq_trans.
 
172
Qed.
 
173
 
 
174
Lemma uniset_twist2 :
 
175
 forall x y z t:uniset,
 
176
   seq (union x (union (union y z) t)) (union (union y (union x z)) t).
 
177
Proof.
 
178
intros; apply seq_trans with (union (union x (union y z)) t).
 
179
apply seq_sym; apply union_ass.
 
180
apply seq_left; apply union_perm_left.
 
181
Qed.
 
182
 
 
183
(** specific for treesort *)
 
184
 
 
185
Lemma treesort_twist1 :
 
186
 forall x y z t u:uniset,
 
187
   seq u (union y z) ->
 
188
   seq (union x (union u t)) (union (union y (union x t)) z).
 
189
Proof.
 
190
intros; apply seq_trans with (union x (union (union y z) t)).
 
191
apply seq_right; apply seq_left; trivial.
 
192
apply uniset_twist1.
 
193
Qed.
 
194
 
 
195
Lemma treesort_twist2 :
 
196
 forall x y z t u:uniset,
 
197
   seq u (union y z) ->
 
198
   seq (union x (union u t)) (union (union y (union x z)) t).
 
199
Proof.
 
200
intros; apply seq_trans with (union x (union (union y z) t)).
 
201
apply seq_right; apply seq_left; trivial.
 
202
apply uniset_twist2.
 
203
Qed.
 
204
 
 
205
 
 
206
(*i theory of minter to do similarly 
 
207
Require Min.
 
208
(* uniset intersection *)
 
209
Definition minter := [m1,m2:uniset]
 
210
    (Charac [a:A](andb (charac m1 a)(charac m2 a))).
 
211
i*)
 
212
 
 
213
End defs.
 
214
 
 
215
Unset Implicit Arguments.
 
 
b'\\ No newline at end of file'