namespace.v 1.83 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.base prelude.countable prelude.co_pset. `````` Ralf Jung committed Feb 08, 2016 2 ``````Require Export program_logic.ownership program_logic.pviewshifts. `````` Robbert Krebbers committed Jan 16, 2016 3 4 5 `````` Definition namespace := list positive. Definition nnil : namespace := nil. `````` Ralf Jung committed Feb 08, 2016 6 7 ``````Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. `````` Ralf Jung committed Feb 08, 2016 8 ``````Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). `````` Robbert Krebbers committed Jan 16, 2016 9 10 `````` Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _). `````` Ralf Jung committed Feb 08, 2016 11 ``````Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed. `````` Robbert Krebbers committed Jan 16, 2016 12 13 ``````Lemma nclose_nnil : nclose nnil = coPset_all. Proof. by apply (sig_eq_pi _). Qed. `````` Ralf Jung committed Feb 08, 2016 14 ``````Lemma encode_nclose N : encode N ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 15 ``````Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. `````` Ralf Jung committed Feb 08, 2016 16 ``````Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 17 18 ``````Proof. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. `````` Ralf Jung committed Feb 08, 2016 19 `````` destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|]. `````` Robbert Krebbers committed Jan 16, 2016 20 21 `````` by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal. Qed. `````` Ralf Jung committed Feb 08, 2016 22 ``````Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 23 ``````Proof. apply nclose_subseteq with x, encode_nclose. Qed. `````` Ralf Jung committed Feb 08, 2016 24 25 ``````Lemma nclose_disjoint `{Countable A} N (x y : A) : x ≠ y → nclose (ndot N x) ∩ nclose (ndot N y) = ∅. `````` Robbert Krebbers committed Jan 16, 2016 26 27 28 29 30 31 32 33 ``````Proof. intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot. rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]]. apply Hxy, (injective encode), (injective encode_nat); revert Hq. rewrite !(list_encode_cons (encode _)). rewrite !(associative_L _) (injective_iff (++ _)%positive) /=. generalize (encode_nat (encode y)). induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver. `````` Ralf Jung committed Feb 08, 2016 34 35 36 37 38 39 ``````Qed. (** Derived forms and lemmas about them. *) Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ := ownI (encode N) P. (* TODO: Add lemmas about inv here. *)``````