coPset.v 17.9 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 iris.prelude Require Export collections.
From iris.prelude 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 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 60
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.
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 102 103 104 105 106 107 108
  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
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 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  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.
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 190 191
  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
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206

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 *)
207 208 209
Lemma coPset_top_subseteq (X : coPset) : X  .
Proof. done. Qed.
Hint Resolve coPset_top_subseteq.
210

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

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

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

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

310 311 312
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.
313 314
Proof. destruct X as [[t ?]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_Pset_finite X : set_finite (of_Pset X).
315
Proof.
316
  apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
317
Qed.
318

319 320 321 322 323 324 325
(** * 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))).

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

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.

335 336 337 338 339 340 341 342 343 344
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.
345
Proof.
346 347 348 349 350 351 352 353 354
  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.
355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
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.
371
  - revert p; induction q; intros [?|?|]; simpl;
372
      rewrite ?coPset_elem_of_node; naive_solver.
373
  - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
374
Qed.
Ralf Jung's avatar
Ralf Jung committed
375 376 377
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
  rewrite coPset_finite_spec; simpl.
378 379
  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
Qed.
Ralf Jung's avatar
Ralf Jung committed
380

381
(** * Splitting of infinite sets *)
382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
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.
399 400 401 402
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 _.
403 404 405 406

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