coPset.v 18.4 KB
Newer Older
1
(* Copyright (c) 2012-2019, 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
From stdpp Require Export sets.
15
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

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.
39
Local Hint Immediate coPNode_wf_l coPNode_wf_r : core.
40 41 42 43 44 45 46

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
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.
50
Hint Resolve coPNode_wf : core.
51 52 53 54 55 56 57 58 59

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 coPset_elem_of_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 coPset_elem_of_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 coPset_elem_of_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 coPset_elem_of_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
Instance coPset_set : Set_ positive coPset.
173 174
Proof.
  split; [split| |].
175
  - by intros ??.
176
  - intros p q. apply coPset_elem_of_singleton.
177
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
178
    by rewrite coPset_elem_of_union, orb_True.
179
  - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
180
    by rewrite coPset_elem_of_intersection, andb_True.
181
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
182 183
    by rewrite coPset_elem_of_intersection,
      coPset_elem_of_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 (@{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 *)
208 209
Lemma coPset_top_subseteq (X : coPset) : X  .
Proof. done. Qed.
210
Hint Resolve coPset_top_subseteq : core.
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
    { destruct b; simpl; [intros [l Hl]|done].
226
      by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
227 228 229 230 231
    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 := default 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
(** * Conversion to psets *)
274
Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
275 276
  match t with
  | coPLeaf _ => PLeaf
277 278
  | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
  | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
279
  end.
280
Lemma coPset_to_Pset_wf t : coPset_wf t  Pmap_wf (coPset_to_Pset_raw t).
281
Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
282 283 284
Definition coPset_to_Pset (X : coPset) : Pset :=
  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
Lemma elem_of_coPset_to_Pset X i : set_finite X  i  coPset_to_Pset X  i  X.
285 286
Proof.
  rewrite coPset_finite_spec; destruct X as [t Ht].
287
  change (coPset_finite t  coPset_to_Pset_raw t !! i = Some ()  e_of i t).
288 289 290 291 292
  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 *)
293
Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
294 295
  match t with
  | PLeaf => coPLeaf false
296 297
  | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
  | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
298
  end.
299
Lemma Pset_to_coPset_wf t : Pmap_wf t  coPset_wf (Pset_to_coPset_raw t).
300 301
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
Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t)  t !! i = Some ().
307
Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
308
Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
309 310
Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.

311 312 313 314 315
Definition Pset_to_coPset (X : Pset) : coPset :=
  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t  Pset_to_coPset_wf _ Ht.
Lemma elem_of_Pset_to_coPset X i : i  Pset_to_coPset X  i  X.
Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
316
Proof.
317
  apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
318
Qed.
319

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

327 328
Definition gset_to_coPset (X : gset positive) : coPset :=
  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t  Pset_to_coPset_wf _ Ht.
329

330
Lemma elem_of_coPset_to_gset X i : set_finite X  i  coPset_to_gset X  i  X.
331
Proof.
332 333
  intros ?. rewrite <-elem_of_coPset_to_Pset by done.
  unfold coPset_to_gset. by destruct (coPset_to_Pset X).
334 335
Qed.

336 337 338
Lemma elem_of_gset_to_coPset X i : i  gset_to_coPset X  i  X.
Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
339
Proof.
340
  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
341 342 343
Qed.

(** * Domain of finite maps *)
344
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
345
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
346
Proof.
347
  split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
348
  by rewrite elem_of_Pset_to_coPset, elem_of_dom.
349
Qed.
350
Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
351
  gset_to_coPset (dom _ m).
352 353 354
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof.
  split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
355
  by rewrite elem_of_gset_to_coPset, 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 coPset_elem_of_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 coPset_elem_of_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.