namespaces.v 3.39 KB
 Robbert Krebbers committed Feb 17, 2016 1 2 3 4 ``````From prelude Require Export countable co_pset. From algebra Require Export base. Definition namespace := list positive. `````` Ralf Jung committed Feb 18, 2016 5 ``````Definition nroot : namespace := nil. `````` Robbert Krebbers committed Feb 17, 2016 6 7 8 9 ``````Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). `````` Ralf Jung committed Feb 22, 2016 10 11 12 ``````Infix ".:" := ndot (at level 19, left associativity) : C_scope. Notation "(.:)" := ndot : C_scope. `````` Robbert Krebbers committed Feb 17, 2016 13 ``````Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _). `````` Robbert Krebbers committed Feb 17, 2016 14 ``````Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed. `````` Ralf Jung committed Feb 18, 2016 15 ``````Lemma nclose_nroot : nclose nroot = ⊤. `````` Robbert Krebbers committed Feb 17, 2016 16 17 18 ``````Proof. by apply (sig_eq_pi _). Qed. Lemma encode_nclose N : encode N ∈ nclose N. Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. `````` Ralf Jung committed Feb 22, 2016 19 ``````Lemma nclose_subseteq `{Countable A} N x : nclose (N .: x) ⊆ nclose N. `````` Robbert Krebbers committed Feb 17, 2016 20 21 ``````Proof. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. `````` Ralf Jung committed Feb 22, 2016 22 `````` destruct (list_encode_suffix N (N .: x)) as [q' ?]; [by exists [encode x]|]. `````` Robbert Krebbers committed Feb 17, 2016 23 24 `````` by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal. Qed. `````` Ralf Jung committed Feb 22, 2016 25 ``````Lemma ndot_nclose `{Countable A} N x : encode (N .: x) ∈ nclose N. `````` Robbert Krebbers committed Feb 17, 2016 26 27 28 29 30 31 32 33 34 35 36 37 38 ``````Proof. apply nclose_subseteq with x, encode_nclose. Qed. Instance ndisjoint : Disjoint namespace := λ N1 N2, ∃ N1' N2', N1' `suffix_of` N1 ∧ N2' `suffix_of` N2 ∧ length N1' = length N2' ∧ N1' ≠ N2'. Section ndisjoint. Context `{Countable A}. Implicit Types x y : A. Global Instance ndisjoint_comm : Comm iff ndisjoint. Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed. `````` Ralf Jung committed Feb 22, 2016 39 40 `````` Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .: x ⊥ N .: y. Proof. intros Hxy. exists (N .: x), (N .: y); naive_solver. Qed. `````` Robbert Krebbers committed Feb 17, 2016 41 `````` `````` Ralf Jung committed Feb 22, 2016 42 `````` Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .: x ⊥ N2. `````` Robbert Krebbers committed Feb 17, 2016 43 44 `````` Proof. intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'. `````` Robbert Krebbers committed Feb 19, 2016 45 `````` split_and?; try done; []. by apply suffix_of_cons_r. `````` Robbert Krebbers committed Feb 17, 2016 46 47 `````` Qed. `````` Ralf Jung committed Feb 22, 2016 48 `````` Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .: x . `````` Robbert Krebbers committed Feb 17, 2016 49 50 51 52 53 54 55 56 57 58 `````` Proof. rewrite ![N1 ⊥ _]comm. apply ndot_preserve_disjoint_l. Qed. Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ∩ nclose N2 = ∅. Proof. intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne). apply elem_of_equiv_empty_L=> p; unfold nclose. rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]]. rewrite !list_encode_app !assoc in Hq. by eapply Hne, list_encode_suffix_eq. Qed. `````` Ralf Jung committed Feb 17, 2016 59 60 61 ``````End ndisjoint. (* This tactic solves goals about inclusion and disjointness `````` Robbert Krebbers committed Feb 17, 2016 62 `````` of masks (i.e., coPsets) with set_solver, taking `````` Ralf Jung committed Feb 17, 2016 63 64 65 66 67 68 `````` disjointness of namespaces into account. *) (* TODO: This tactic is by far now yet as powerful as it should be. For example, given N1 ⊥ N2, it should be able to solve nclose (ndot N1 x) ∩ N2 ≡ ∅. It should also solve (ndot N x) ∩ (ndot N y) ≡ ∅ if x ≠ y is in the context or follows from [discriminate]. *) `````` Robbert Krebbers committed Feb 17, 2016 69 ``````Ltac set_solver_ndisj := `````` Ralf Jung committed Feb 17, 2016 70 71 72 73 `````` repeat match goal with (* TODO: Restrict these to have type namespace *) | [ H : (?N1 ⊥ ?N2) |-_ ] => apply ndisj_disjoint in H end; `````` Robbert Krebbers committed Feb 17, 2016 74 `````` set_solver. `````` Ralf Jung committed Feb 17, 2016 75 ``````(* TODO: restrict this to match only if this is ⊆ of coPset *) `````` Robbert Krebbers committed Feb 17, 2016 76 ``````Hint Extern 500 (_ ⊆ _) => set_solver_ndisj : ndisj. `````` Ralf Jung committed Feb 17, 2016 77 78 79 80 81 82 ``````(* The hope is that registering these will suffice to solve most goals of the form N1 ⊥ N2. TODO: Can this prove x ≠ y if discriminate can? *) Hint Resolve ndot_ne_disjoint : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_r : ndisj.``````