From 2420784dd1e938d0706320b477de1828d93afeb2 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 11 Dec 2015 15:31:33 +0100 Subject: [PATCH] More on finite/cofinite sets of positives. --- prelude/co_pset.v | 206 ++++++++++++++++++++++++++++++---------------- prelude/numbers.v | 4 +- 2 files changed, 140 insertions(+), 70 deletions(-) diff --git a/prelude/co_pset.v b/prelude/co_pset.v index 85115bc1a..d00c218df 100644 --- a/prelude/co_pset.v +++ b/prelude/co_pset.v @@ -10,7 +10,6 @@ Local Open Scope positive_scope. 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. @@ -49,7 +48,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool := end. Local Notation e_of := coPset_elem_of_raw. Arguments coPset_elem_of_raw _ !_ / : simpl nomatch. -Lemma coPset_elem_of_coPNode' b l r p : +Lemma coPset_elem_of_node b l r p : e_of p (coPNode' b l r) = e_of p (coPNode b l r). Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed. @@ -86,9 +85,9 @@ Instance coPset_union_raw : Union coPset_raw := | coPLeaf false, coPLeaf false => coPLeaf false | _, coPLeaf true => coPLeaf true | coPLeaf true, _ => coPLeaf true - | 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) + | 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) end. Local Arguments union _ _!_ !_ /. Instance coPset_intersection_raw : Intersection coPset_raw := @@ -97,9 +96,9 @@ Instance coPset_intersection_raw : Intersection coPset_raw := | coPLeaf true, coPLeaf true => coPLeaf true | _, coPLeaf false => coPLeaf false | coPLeaf false, _ => coPLeaf false - | 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) + | 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) end. Local Arguments intersection _ _!_ !_ /. Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw := @@ -117,29 +116,29 @@ Lemma coPset_intersection_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. -Lemma elem_of_coPset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q. +Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q. Proof. - split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_coPNode']. + split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node]. by revert q; induction p; intros [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; intros; f_equal'; auto. + rewrite ?coPset_elem_of_node; intros; f_equal'; auto. Qed. -Lemma elem_of_coPset_union t1 t2 p : e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2. +Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2. Proof. by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; simpl; + rewrite ?coPset_elem_of_node; simpl; rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r. Qed. -Lemma elem_of_coPset_intersection t1 t2 p : +Lemma elem_to_Pset_intersection t1 t2 p : e_of p (t1 ∩ t2) = e_of p t1 && e_of p t2. Proof. by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; simpl; + rewrite ?coPset_elem_of_node; simpl; rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r. Qed. -Lemma elem_of_coPset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t). +Lemma elem_to_Pset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t). Proof. by revert p; induction t as [[]|[]]; intros [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; simpl. + rewrite ?coPset_elem_of_node; simpl. Qed. (** * Packed together + set operations *) @@ -165,14 +164,14 @@ Instance coPset_collection : Collection positive coPset. Proof. split; [split| |]. * by intros ??. - * intros p q. apply elem_of_coPset_singleton. + * intros p q. apply elem_to_Pset_singleton. * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl. - by rewrite elem_of_coPset_union, orb_True. + by rewrite elem_to_Pset_union, orb_True. * intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl. - by rewrite elem_of_coPset_intersection, andb_True. + by rewrite elem_to_Pset_intersection, andb_True. * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl. - by rewrite elem_of_coPset_intersection, - elem_of_coPset_opp, andb_True, negb_True. + by rewrite elem_to_Pset_intersection, + elem_to_Pset_opp, andb_True, negb_True. Qed. Instance coPset_leibniz : LeibnizEquiv coPset. Proof. @@ -181,18 +180,111 @@ Proof. intros p; apply eq_bool_prop_intro, (HXY p). Qed. -(** Infinite sets *) -Fixpoint coPset_infinite_raw (t : coPset_raw) : bool := +(** * Finite sets *) +Fixpoint coPset_finite (t : coPset_raw) : bool := match t with - | coPLeaf b => b - | coPNode b l r => coPset_infinite_raw l || coPset_infinite_raw r + | coPLeaf b => negb b | coPNode b l r => coPset_finite l && coPset_finite r end. -Definition coPset_infinite (t : coPset) : bool := coPset_infinite_raw (`t). -Lemma coPset_infinite_coPNode b l r : - coPset_infinite_raw (coPNode' b l r) = coPset_infinite_raw (coPNode b l r). +Lemma coPset_finite_node b l r : + coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r. Proof. by destruct b, l as [[]|], r as [[]|]. Qed. +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. + * induction t as [b|b l IHl r IHr]; simpl. + { 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. + * induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|]. + 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. + +(** * 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. + * intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto. + * destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r; + rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition. +Qed. +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. +Proof. + destruct X as [[t Ht]]; change (e_of i (of_Pset_raw t) ↔ t !! i = Some ()). + clear Ht; revert i. + induction t as [|[[]|] l IHl r IHr]; intros [i|i|]; simpl; auto; by split. +Qed. +Lemma of_Pset_finite X : set_finite (of_Pset X). +Proof. + rewrite coPset_finite_spec; destruct X as [[t Ht]]; simpl; clear Ht. + induction t as [|[[]|] l IHl r IHr]; simpl; rewrite ?andb_True; auto. +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. + * revert p; induction q; intros [?|?|]; simpl; + rewrite ?coPset_elem_of_node; naive_solver. + * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node. +Qed. -(** Splitting of infinite sets *) +(** * Domain of finite maps *) +Instance Pmap_dom_Pset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m). +Instance Pmap_dom_coPset: FinMapDom positive Pmap coPset. +Proof. + split; try apply _; intros A m i; unfold dom, Pmap_dom_Pset. + by rewrite elem_of_of_Pset, elem_of_dom. +Qed. + +(** * Splitting of infinite sets *) Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw := match t with | coPLeaf false => coPLeaf false @@ -218,57 +310,33 @@ Definition coPset_r (X : coPset) : coPset := Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅. Proof. apply elem_of_equiv_empty_L; intros p; apply Is_true_false. - destruct X as [t Ht]; simpl; clear Ht; rewrite elem_of_coPset_intersection. + destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_intersection. revert p; induction t as [[]|[]]; intros [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; simpl; + rewrite ?coPset_elem_of_node; simpl; 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. - destruct X as [t Ht]; simpl; clear Ht; rewrite elem_of_coPset_union. + destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_union. revert p; induction t as [[]|[]]; intros [?|?|]; simpl; - rewrite ?coPset_elem_of_coPNode'; simpl; + rewrite ?coPset_elem_of_node; simpl; rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto. Qed. -Lemma coPset_l_infinite X : coPset_infinite X → coPset_infinite (coPset_l X). -Proof. - destruct X as [t Ht]; unfold coPset_infinite; simpl; clear Ht. - induction t as [[]|]; simpl; - rewrite ?coPset_infinite_coPNode; simpl; rewrite ?orb_True; tauto. -Qed. -Lemma coPset_r_infinite X : coPset_infinite X → coPset_infinite (coPset_r X). -Proof. - destruct X as [t Ht]; unfold coPset_infinite; simpl; clear Ht. - induction t as [[]|]; simpl; - rewrite ?coPset_infinite_coPNode; simpl; rewrite ?orb_True; tauto. -Qed. - -(** Conversion from psets *) -Fixpoint to_coPset_raw (t : Pmap_raw ()) : coPset_raw := - match t with - | PLeaf => coPLeaf false - | PNode None l r => coPNode false (to_coPset_raw l) (to_coPset_raw r) - | PNode (Some _) l r => coPNode true (to_coPset_raw l) (to_coPset_raw r) - end. -Lemma to_coPset_raw_wf t : Pmap_wf t → coPset_wf (to_coPset_raw t). +Lemma coPset_l_finite X : set_finite (coPset_l X) → set_finite X. Proof. - induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto. - * intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto. - * destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r; - rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition. + rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht. + induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto. Qed. -Definition to_coPset (X : Pset) : coPset := - let (m) := X in let (t,Ht) := m in to_coPset_raw t ↾ to_coPset_raw_wf _ Ht. -Lemma elem_of_to_coPset X i : i ∈ to_coPset X ↔ i ∈ X. +Lemma coPset_r_finite X : set_finite (coPset_r X) → set_finite X. Proof. - destruct X as [[t Ht]]; change (e_of i (to_coPset_raw t) ↔ t !! i = Some ()). - clear Ht; revert i. - induction t as [|[[]|] l IHl r IHr]; intros [i|i|]; simpl; auto; by split. + rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht. + induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto. Qed. -Instance Pmap_dom_Pset {A} : Dom (Pmap A) coPset := λ m, to_coPset (dom _ m). -Instance Pmap_dom_coPset: FinMapDom positive Pmap coPset. +Lemma coPset_split X : + ¬set_finite X → + ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ ¬set_finite X1 ∧ ¬set_finite X2. Proof. - split; try apply _; intros A m i; unfold dom, Pmap_dom_Pset. - by rewrite elem_of_to_coPset, elem_of_dom. + exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union, + coPset_lr_disjoint, coPset_l_finite, coPset_r_finite. Qed. diff --git a/prelude/numbers.v b/prelude/numbers.v index 8c7da83aa..2a2c038b1 100644 --- a/prelude/numbers.v +++ b/prelude/numbers.v @@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful notations. *) Require Export Eqdep PArith NArith ZArith NPeano. Require Import QArith Qcanon. -Require Export prelude.base prelude.decidable. +Require Export prelude.base prelude.decidable prelude.option. Open Scope nat_scope. Coercion Z.of_nat : nat >-> Z. @@ -108,6 +108,8 @@ Arguments Pos.of_nat _ : simpl never. Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec. Instance positive_inhabited: Inhabited positive := populate 1. +Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end. +Instance maybe_x1 : Maybe xI := λ p, match p with p~1 => Some p | _ => None end. Instance: Injective (=) (=) (~0). Proof. by injection 1. Qed. Instance: Injective (=) (=) (~1). -- GitLab