coPset.v 17.5 KB
Newer Older
1
2
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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
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
Local Open Scope positive_scope.

(** * The tree data structure *)
Inductive coPset_raw :=
  | coPLeaf : bool  coPset_raw
  | coPNode : bool  coPset_raw  coPset_raw  coPset_raw.
Instance coPset_raw_eq_dec (t1 t2 : coPset_raw) : Decision (t1 = t2).
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.
Arguments coPset_wf !_ / : simpl nomatch.

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.
Arguments coPNode' _ _ _ : simpl never.
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.
Arguments coPset_elem_of_raw _ !_ / : simpl nomatch.
60
Lemma coPset_elem_of_node b l r p :
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
  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 *.
77
78
79
80
  - 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)| |].
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
    + 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
97
98
99
  | 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)
100
101
102
103
104
105
106
107
  end.
Local Arguments union _ _!_ !_ /.
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
108
109
110
  | 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)
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
  end.
Local Arguments intersection _ _!_ !_ /.
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.
128
Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q)  p = q.
129
Proof.
130
  split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
131
  by revert q; induction p; intros [?|?|]; simpl;
132
    rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
133
Qed.
134
Lemma elem_to_Pset_union t1 t2 p : e_of p (t1  t2) = e_of p t1 || e_of p t2.
135
136
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
137
    rewrite ?coPset_elem_of_node; simpl;
138
139
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r.
Qed.
140
Lemma elem_to_Pset_intersection t1 t2 p :
141
142
143
  e_of p (t1  t2) = e_of p t1 && e_of p t2.
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
144
    rewrite ?coPset_elem_of_node; simpl;
145
146
    rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r.
Qed.
147
Lemma elem_to_Pset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
148
149
Proof.
  by revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
150
    rewrite ?coPset_elem_of_node; simpl.
151
152
153
154
155
156
157
158
159
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.
160
Instance coPset_top : Top coPset := coPLeaf true  I.
161
Instance coPset_union : Union coPset := λ X Y,
162
163
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  t2)  coPset_union_wf _ _ Ht1 Ht2.
164
Instance coPset_intersection : Intersection coPset := λ X Y,
165
166
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  t2)  coPset_intersection_wf _ _ Ht1 Ht2.
167
Instance coPset_difference : Difference coPset := λ X Y,
168
169
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1  coPset_opp_raw t2)  coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
170
171
172
173

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

185
186
Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
187
  intros X Y; rewrite elem_of_equiv; intros HXY.
188
189
190
  apply (sig_eq_pi _), coPset_eq; try apply proj2_sig.
  intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205

Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p  X) := _.
Instance coPset_equiv_dec (X Y : coPset) : Decision (X  Y).
Proof. refine (cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Instance mapset_disjoint_dec (X Y : coPset) : Decision (X  Y).
Proof.
 refine (cast_if (decide (X  Y = )));
  abstract (by rewrite disjoint_intersection_L).
Defined.
Instance mapset_subseteq_dec (X Y : coPset) : Decision (X  Y).
Proof.
 refine (cast_if (decide (X  Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.

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

210
211
(** * Finite sets *)
Fixpoint coPset_finite (t : coPset_raw) : bool :=
212
  match t with
213
  | coPLeaf b => negb b | coPNode b l r => coPset_finite l && coPset_finite r
214
  end.
215
216
Lemma coPset_finite_node b l r :
  coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
217
Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
218
219
220
221
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.
222
  - induction t as [b|b l IHl r IHr]; simpl.
223
224
225
226
227
228
229
    { 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.
230
  - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
231
232
233
234
235
236
237
238
239
    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.

240
241
242
(** * Pick element from infinite sets *)
(* Implemented using depth-first search, which results in very unbalanced
trees. *)
243
244
245
246
247
248
249
250
251
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.
252
Definition coPpick (X : coPset) : positive := from_option id 1 (coPpick_raw (`X)).
253
254
255

Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i  e_of i t.
Proof.
256
257
  revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_eq/=; auto.
  destruct (coPpick_raw l); simplify_option_eq; auto.
258
259
260
Qed.
Lemma coPpick_raw_None t : coPpick_raw t = None  coPset_finite t.
Proof.
261
262
  induction t as [[]|[] l ? r]; intros i; simplify_eq/=; auto.
  destruct (coPpick_raw l); simplify_option_eq; auto.
263
264
265
266
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:?.
267
268
  - by intros; apply coPpick_raw_elem_of.
  - by intros []; apply coPset_finite_spec, coPpick_raw_None.
269
270
Qed.

271
272
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
(** * 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.
300
301
  - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
  - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
302
303
      rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
Qed.
304
305
306
307
308
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.

309
310
311
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.
312
313
Proof. destruct X as [[t ?]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_Pset_finite X : set_finite (of_Pset X).
314
Proof.
315
  apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
316
Qed.
317
318
319
320
321
322
323
324
325
326
327
328
329
330

(** * Conversion from gsets of positives *)
Definition of_gset (X : gset positive) : coPset :=
  let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t  of_Pset_wf _ Ht.
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 *)
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
331
Proof.
332
333
334
335
336
337
338
339
340
  split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
  by rewrite elem_of_of_Pset, elem_of_dom.
Qed.
Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
  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.
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
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.
357
  - revert p; induction q; intros [?|?|]; simpl;
358
      rewrite ?coPset_elem_of_node; naive_solver.
359
  - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
360
Qed.
Ralf Jung's avatar
Ralf Jung committed
361
362
363
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
  rewrite coPset_finite_spec; simpl.
364
365
  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
366

367
(** * Splitting of infinite sets *)
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
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.
385
386
387
388
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 _.
389
390
391
392

Lemma coPset_lr_disjoint X : coPset_l X  coPset_r X = .
Proof.
  apply elem_of_equiv_empty_L; intros p; apply Is_true_false.
393
  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_intersection.
394
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
395
    rewrite ?coPset_elem_of_node; simpl;
396
397
398
399
400
    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.
401
  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_union.
402
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
403
    rewrite ?coPset_elem_of_node; simpl;
404
405
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
Qed.
406
Lemma coPset_l_finite X : set_finite (coPset_l X)  set_finite X.
407
Proof.
408
409
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
410
Qed.
411
Lemma coPset_r_finite X : set_finite (coPset_r X)  set_finite X.
412
Proof.
413
414
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
415
Qed.
416
417
418
Lemma coPset_split X :
  ¬set_finite X 
   X1 X2, X = X1  X2  X1  X2 =   ¬set_finite X1  ¬set_finite X2.
419
Proof.
420
421
  exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
    coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
422
Qed.