coPset.v 18 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
4
5
6
7
8
9
10
11
12
13
(** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are:

- Closed under union, intersection and set complement.
- Closed under splitting of cofinite sets.

Also, they enjoy various nice properties, such as decidable equality and set
membership, as well as extensional equality (i.e. [X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y]).

Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *)
14
15
From stdpp Require Export collections.
From stdpp Require Import pmap gmap mapset.
16
Set Default Proof Using "Type".
17
18
19
20
21
22
Local Open Scope positive_scope.

(** * The tree data structure *)
Inductive coPset_raw :=
  | coPLeaf : bool  coPset_raw
  | coPNode : bool  coPset_raw  coPset_raw  coPset_raw.
23
Instance coPset_raw_eq_dec : EqDecision coPset_raw.
24
25
26
27
28
29
30
31
32
Proof. solve_decision. Defined.

Fixpoint coPset_wf (t : coPset_raw) : bool :=
  match t with
  | coPLeaf _ => true
  | coPNode true (coPLeaf true) (coPLeaf true) => false
  | coPNode false (coPLeaf false) (coPLeaf false) => false
  | coPNode b l r => coPset_wf l && coPset_wf r
  end.
33
Arguments coPset_wf !_ / : simpl nomatch, assert.
34
35
36
37
38
39
40
41
42
43
44
45
46

Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r)  coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r)  coPset_wf r.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate coPNode_wf_l coPNode_wf_r.

Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
  match b, l, r with
  | true, coPLeaf true, coPLeaf true => coPLeaf true
  | false, coPLeaf false, coPLeaf false => coPLeaf false
  | _, _, _ => coPNode b l r
  end.
47
Arguments coPNode' : simpl never.
48
49
50
51
52
53
54
55
56
57
58
59
Lemma coPNode_wf b l r : coPset_wf l  coPset_wf r  coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
Hint Resolve coPNode_wf.

Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
  match t, p with
  | coPLeaf b, _ => b
  | coPNode b l r, 1 => b
  | coPNode _ l _, p~0 => coPset_elem_of_raw p l
  | coPNode _ _ r, p~1 => coPset_elem_of_raw p r
  end.
Local Notation e_of := coPset_elem_of_raw.
60
Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
61
Lemma coPset_elem_of_node b l r p :
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  e_of p (coPNode' b l r) = e_of p (coPNode b l r).
Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.

Lemma coPLeaf_wf t b : ( p, e_of p t = b)  coPset_wf t  t = coPLeaf b.
Proof.
  induction t as [b'|b' l IHl r IHr]; intros Ht ?; [f_equal; apply (Ht 1)|].
  assert (b' = b) by (apply (Ht 1)); subst.
  assert (l = coPLeaf b) as -> by (apply IHl; try apply (λ p, Ht (p~0)); eauto).
  assert (r = coPLeaf b) as -> by (apply IHr; try apply (λ p, Ht (p~1)); eauto).
  by destruct b.
Qed.
Lemma coPset_eq t1 t2 :
  ( p, e_of p t1 = e_of p t2)  coPset_wf t1  coPset_wf t2  t1 = t2.
Proof.
  revert t2.
  induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *.
78
79
80
81
  - f_equal; apply (Ht 1).
  - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
  - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
  - f_equal; [apply (Ht 1)| |].
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
    + apply IHl; try apply (λ x, Ht (x~0)); eauto.
    + apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.

Fixpoint coPset_singleton_raw (p : positive) : coPset_raw :=
  match p with
  | 1 => coPNode true (coPLeaf false) (coPLeaf false)
  | p~0 => coPNode' false (coPset_singleton_raw p) (coPLeaf false)
  | p~1 => coPNode' false (coPLeaf false) (coPset_singleton_raw p)
  end.
Instance coPset_union_raw : Union coPset_raw :=
  fix go t1 t2 := let _ : Union _ := @go in
  match t1, t2 with
  | coPLeaf false, coPLeaf false => coPLeaf false
  | _, coPLeaf true => coPLeaf true
  | coPLeaf true, _ => coPLeaf true
98
99
100
  | coPNode b l r, coPLeaf false => coPNode b l r
  | coPLeaf false, coPNode b l r => coPNode b l r
  | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1  l2) (r1  r2)
101
  end.
102
Local Arguments union _ _!_ !_ / : assert.
103
104
105
106
107
108
Instance coPset_intersection_raw : Intersection coPset_raw :=
  fix go t1 t2 := let _ : Intersection _ := @go in
  match t1, t2 with
  | coPLeaf true, coPLeaf true => coPLeaf true
  | _, coPLeaf false => coPLeaf false
  | coPLeaf false, _ => coPLeaf false
109
110
111
  | coPNode b l r, coPLeaf true => coPNode b l r
  | coPLeaf true, coPNode b l r => coPNode b l r
  | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1&&b2) (l1  l2) (r1  r2)
112
  end.
113
Local Arguments intersection _ _!_ !_ / : assert.
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw :=
  match t with
  | coPLeaf b => coPLeaf (negb b)
  | coPNode b l r => coPNode' (negb b) (coPset_opp_raw l) (coPset_opp_raw r)
  end.

Lemma coPset_singleton_wf p : coPset_wf (coPset_singleton_raw p).
Proof. induction p; simpl; eauto. Qed.
Lemma coPset_union_wf t1 t2 : coPset_wf t1  coPset_wf t2  coPset_wf (t1  t2).
Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
Lemma coPset_intersection_wf t1 t2 :
  coPset_wf t1  coPset_wf t2  coPset_wf (t1  t2).
Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
Proof. induction t as [[]|[]]; simpl; eauto. Qed.
129
Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q)  p = q.
130
Proof.
131
  split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
132
  by revert q; induction p; intros [?|?|]; simpl;
133
    rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
134
Qed.
135
Lemma elem_to_Pset_union t1 t2 p : e_of p (t1  t2) = e_of p t1 || e_of p t2.
136
137
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
138
    rewrite ?coPset_elem_of_node; simpl;
139
140
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r.
Qed.
141
Lemma elem_to_Pset_intersection t1 t2 p :
142
143
144
  e_of p (t1  t2) = e_of p t1 && e_of p t2.
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
145
    rewrite ?coPset_elem_of_node; simpl;
146
147
    rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r.
Qed.
148
Lemma elem_to_Pset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
149
150
Proof.
  by revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
151
    rewrite ?coPset_elem_of_node; simpl.
152
153
154
155
156
157
158
159
160
Qed.

(** * Packed together + set operations *)
Definition coPset := { t | coPset_wf t }.

Instance coPset_singleton : Singleton positive coPset := λ p,
  coPset_singleton_raw p  coPset_singleton_wf _.
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false  I.
161
Instance coPset_top : Top coPset := coPLeaf true  I.
162
Instance coPset_union : Union coPset := λ X Y,
163
164
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  t2)  coPset_union_wf _ _ Ht1 Ht2.
165
Instance coPset_intersection : Intersection coPset := λ X Y,
166
167
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  t2)  coPset_intersection_wf _ _ Ht1 Ht2.
168
Instance coPset_difference : Difference coPset := λ X Y,
169
170
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  coPset_opp_raw t2)  coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
171
172
173
174

Instance coPset_collection : Collection positive coPset.
Proof.
  split; [split| |].
175
176
177
  - by intros ??.
  - intros p q. apply elem_to_Pset_singleton.
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
178
    by rewrite elem_to_Pset_union, orb_True.
179
  - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
180
    by rewrite elem_to_Pset_intersection, andb_True.
181
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
182
183
    by rewrite elem_to_Pset_intersection,
      elem_to_Pset_opp, andb_True, negb_True.
184
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
185

186
187
Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
188
  intros X Y; rewrite elem_of_equiv; intros HXY.
189
  apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
190
191
  intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
192

Robbert Krebbers's avatar
Robbert Krebbers committed
193
Instance coPset_elem_of_dec : RelDecision (@{coPset}).
194
Proof. solve_decision. Defined.
195
Instance coPset_equiv_dec : RelDecision (@{coPset}).
196
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Proof.
199
 refine (λ X Y, cast_if (decide (X  Y = )));
Robbert Krebbers's avatar
Robbert Krebbers committed
200
201
  abstract (by rewrite disjoint_intersection_L).
Defined.
202
Instance mapset_subseteq_dec : RelDecision (@subseteq coPset _).
Robbert Krebbers's avatar
Robbert Krebbers committed
203
Proof.
204
 refine (λ X Y, cast_if (decide (X  Y = Y))); abstract (by rewrite subseteq_union_L).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
Defined.

(** * Top *)
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209
210
Lemma coPset_top_subseteq (X : coPset) : X  .
Proof. done. Qed.
Hint Resolve coPset_top_subseteq.
211

212
213
(** * Finite sets *)
Fixpoint coPset_finite (t : coPset_raw) : bool :=
214
  match t with
215
  | coPLeaf b => negb b | coPNode b l r => coPset_finite l && coPset_finite r
216
  end.
217
218
Lemma coPset_finite_node b l r :
  coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
219
Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
220
221
222
223
Lemma coPset_finite_spec X : set_finite X  coPset_finite (`X).
Proof.
  destruct X as [t Ht].
  unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
224
  - induction t as [b|b l IHl r IHr]; simpl.
225
226
227
228
229
230
231
    { destruct b; simpl; [intros [l Hl]|done].
      by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. }
    intros [ll Hll]; rewrite andb_True; split.
    + apply IHl; exists (omap (maybe (~0)) ll); intros i.
      rewrite elem_of_list_omap; intros; exists (i~0); auto.
    + apply IHr; exists (omap (maybe (~1)) ll); intros i.
      rewrite elem_of_list_omap; intros; exists (i~1); auto.
232
  - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
233
234
235
236
237
238
239
240
241
    rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto.
    exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
      rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
Qed.
Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
Proof.
  refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
Defined.

242
243
244
(** * Pick element from infinite sets *)
(* Implemented using depth-first search, which results in very unbalanced
trees. *)
245
246
247
248
249
250
251
252
253
Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
  match t with
  | coPLeaf true | coPNode true _ _ => Some 1
  | coPLeaf false => None
  | coPNode false l r =>
     match coPpick_raw l with
     | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
     end
  end.
254
Definition coPpick (X : coPset) : positive := from_option id 1 (coPpick_raw (`X)).
255
256
257

Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i  e_of i t.
Proof.
258
259
  revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_eq/=; auto.
  destruct (coPpick_raw l); simplify_option_eq; auto.
260
261
262
Qed.
Lemma coPpick_raw_None t : coPpick_raw t = None  coPset_finite t.
Proof.
263
264
  induction t as [[]|[] l ? r]; intros i; simplify_eq/=; auto.
  destruct (coPpick_raw l); simplify_option_eq; auto.
265
266
267
268
Qed.
Lemma coPpick_elem_of X : ¬set_finite X  coPpick X  X.
Proof.
  destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?.
269
270
  - by intros; apply coPpick_raw_elem_of.
  - by intros []; apply coPset_finite_spec, coPpick_raw_None.
271
272
Qed.

273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
(** * Conversion to psets *)
Fixpoint to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
  match t with
  | coPLeaf _ => PLeaf
  | coPNode false l r => PNode' None (to_Pset_raw l) (to_Pset_raw r)
  | coPNode true l r => PNode (Some ()) (to_Pset_raw l) (to_Pset_raw r)
  end.
Lemma to_Pset_wf t : coPset_wf t  Pmap_wf (to_Pset_raw t).
Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
Definition to_Pset (X : coPset) : Pset :=
  let (t,Ht) := X in Mapset (PMap (to_Pset_raw t) (to_Pset_wf _ Ht)).
Lemma elem_of_to_Pset X i : set_finite X  i  to_Pset X  i  X.
Proof.
  rewrite coPset_finite_spec; destruct X as [t Ht].
  change (coPset_finite t  to_Pset_raw t !! i = Some ()  e_of i t).
  clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
    simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
Qed.

(** * Conversion from psets *)
Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw :=
  match t with
  | PLeaf => coPLeaf false
  | PNode None l r => coPNode false (of_Pset_raw l) (of_Pset_raw r)
  | PNode (Some _) l r => coPNode true (of_Pset_raw l) (of_Pset_raw r)
  end.
Lemma of_Pset_wf t : Pmap_wf t  coPset_wf (of_Pset_raw t).
Proof.
  induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
302
303
  - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
  - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
304
305
      rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
Qed.
306
307
308
309
310
Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t)  t !! i = Some ().
Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
Lemma of_Pset_raw_finite t : coPset_finite (of_Pset_raw t).
Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.

311
312
313
Definition of_Pset (X : Pset) : coPset :=
  let 'Mapset (PMap t Ht) := X in of_Pset_raw t  of_Pset_wf _ Ht.
Lemma elem_of_of_Pset X i : i  of_Pset X  i  X.
314
315
Proof. destruct X as [[t ?]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_Pset_finite X : set_finite (of_Pset X).
316
Proof.
317
  apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
318
Qed.
319

320
321
322
323
324
325
326
(** * Conversion to and from gsets of positives *)
Lemma to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
Proof. done. Qed.
Definition to_gset (X : coPset) : gset positive :=
  let 'Mapset m := to_Pset X in
  Mapset (GMap m (bool_decide_pack _ (to_gset_wf m))).

327
328
Definition of_gset (X : gset positive) : coPset :=
  let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t  of_Pset_wf _ Ht.
329
330
331
332
333
334
335

Lemma elem_of_to_gset X i : set_finite X  i  to_gset X  i  X.
Proof.
  intros ?. rewrite <-elem_of_to_Pset by done.
  unfold to_gset. by destruct (to_Pset X).
Qed.

336
337
338
339
340
341
342
343
Lemma elem_of_of_gset X i : i  of_gset X  i  X.
Proof. destruct X as [[[t ?]]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_gset_finite X : set_finite (of_gset X).
Proof.
  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply of_Pset_raw_finite.
Qed.

(** * Domain of finite maps *)
344
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
345
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
346
Proof.
347
348
349
  split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
  by rewrite elem_of_of_Pset, elem_of_dom.
Qed.
350
Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
351
352
353
354
355
  of_gset (dom _ m).
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof.
  split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
  by rewrite elem_of_of_gset, elem_of_dom.
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
Qed.

(** * Suffix sets *)
Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
  match p with
  | 1 => coPLeaf true
  | p~0 => coPNode' false (coPset_suffixes_raw p) (coPLeaf false)
  | p~1 => coPNode' false (coPLeaf false) (coPset_suffixes_raw p)
  end.
Lemma coPset_suffixes_wf p : coPset_wf (coPset_suffixes_raw p).
Proof. induction p; simpl; eauto. Qed.
Definition coPset_suffixes (p : positive) : coPset :=
  coPset_suffixes_raw p  coPset_suffixes_wf _.
Lemma elem_coPset_suffixes p q : p  coPset_suffixes q   q', p = q' ++ q.
Proof.
  unfold elem_of, coPset_elem_of; simpl; split.
372
  - revert p; induction q; intros [?|?|]; simpl;
373
      rewrite ?coPset_elem_of_node; naive_solver.
374
  - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
375
Qed.
Ralf Jung's avatar
Ralf Jung committed
376
377
378
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
  rewrite coPset_finite_spec; simpl.
379
380
  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
381

382
(** * Splitting of infinite sets *)
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
  match t with
  | coPLeaf false => coPLeaf false
  | coPLeaf true => coPNode true (coPLeaf true) (coPLeaf false)
  | coPNode b l r => coPNode' b (coPset_l_raw l) (coPset_l_raw r)
  end.
Fixpoint coPset_r_raw (t : coPset_raw) : coPset_raw :=
  match t with
  | coPLeaf false => coPLeaf false
  | coPLeaf true => coPNode false (coPLeaf false) (coPLeaf true)
  | coPNode b l r => coPNode' false (coPset_r_raw l) (coPset_r_raw r)
  end.

Lemma coPset_l_wf t : coPset_wf (coPset_l_raw t).
Proof. induction t as [[]|]; simpl; auto. Qed.
Lemma coPset_r_wf t : coPset_wf (coPset_r_raw t).
Proof. induction t as [[]|]; simpl; auto. Qed.
400
401
402
403
Definition coPset_l (X : coPset) : coPset :=
  let (t,Ht) := X in coPset_l_raw t  coPset_l_wf _.
Definition coPset_r (X : coPset) : coPset :=
  let (t,Ht) := X in coPset_r_raw t  coPset_r_wf _.
404
405
406
407

Lemma coPset_lr_disjoint X : coPset_l X  coPset_r X = .
Proof.
  apply elem_of_equiv_empty_L; intros p; apply Is_true_false.
408
  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_intersection.
409
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
410
    rewrite ?coPset_elem_of_node; simpl;
411
412
413
414
415
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
Qed.
Lemma coPset_lr_union X : coPset_l X  coPset_r X = X.
Proof.
  apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
416
  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_union.
417
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
418
    rewrite ?coPset_elem_of_node; simpl;
419
420
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
Qed.
421
Lemma coPset_l_finite X : set_finite (coPset_l X)  set_finite X.
422
Proof.
423
424
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
425
Qed.
426
Lemma coPset_r_finite X : set_finite (coPset_r X)  set_finite X.
427
Proof.
428
429
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
430
Qed.
431
Lemma coPset_split (X : coPset) :
432
433
  ¬set_finite X 
   X1 X2, X = X1  X2  X1  X2 =   ¬set_finite X1  ¬set_finite X2.
434
Proof.
435
436
  exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
    coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
437
Qed.