namespace.v 1.83 KB
Newer Older
1
Require Export algebra.base prelude.countable prelude.co_pset.
2
Require Export program_logic.ownership program_logic.pviewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5

Definition namespace := list positive.
Definition nnil : namespace := nil.
6
7
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
  encode x :: N.
Ralf Jung's avatar
Ralf Jung committed
8
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10

Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
11
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
14
Lemma encode_nclose N : encode N  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
16
Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
Proof.
  intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
19
  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
  by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
Qed.
22
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
24
25
Lemma nclose_disjoint `{Countable A} N (x y : A) :
  x  y  nclose (ndot N x)  nclose (ndot N y) = .
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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. *)