namespaces.v 2.91 KB
Newer Older
1 2
From iris.prelude Require Export countable co_pset.
From iris.algebra Require Export base.
3 4

Definition namespace := list positive.
5
Definition nroot : namespace := nil.
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's avatar
Ralf Jung committed
10 11
Infix ".@" := ndot (at level 19, left associativity) : C_scope.
Notation "(.@)" := ndot (only parsing) : C_scope.
Ralf Jung's avatar
Ralf Jung committed
12

13
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
14
Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
15
Lemma nclose_nroot : nclose nroot = .
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's avatar
Ralf Jung committed
19
Lemma nclose_subseteq `{Countable A} N x : nclose (N .@ x)  nclose N.
20 21
Proof.
  intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
Ralf Jung's avatar
Ralf Jung committed
22
  destruct (list_encode_suffix N (N .@ x)) as [q' ?]; [by exists [encode x]|].
23 24
  by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Ralf Jung's avatar
Ralf Jung committed
25
Lemma ndot_nclose `{Countable A} N x : encode (N .@ x)  nclose N.
26 27 28 29 30
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'.
31
Typeclasses Opaque ndisjoint.
32 33 34 35 36 37 38 39

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.

40
  Lemma ndot_ne_disjoint N x y : x  y  N .@ x  N .@ y.
Ralf Jung's avatar
Ralf Jung committed
41
  Proof. intros Hxy. exists (N .@ x), (N .@ y); naive_solver. Qed.
42

Ralf Jung's avatar
Ralf Jung committed
43
  Lemma ndot_preserve_disjoint_l N1 N2 x : N1  N2  N1 .@ x  N2.
44 45
  Proof.
    intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
46
    split_and?; try done; []. by apply suffix_of_cons_r.
47 48
  Qed.

Ralf Jung's avatar
Ralf Jung committed
49
  Lemma ndot_preserve_disjoint_r N1 N2 x : N1  N2  N1  N2 .@ x .
50 51
  Proof. rewrite ![N1  _]comm. apply ndot_preserve_disjoint_l. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
52
  Lemma ndisj_disjoint N1 N2 : N1  N2  nclose N1  nclose N2.
53
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56
    intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne) p; unfold nclose.
    rewrite !elem_coPset_suffixes; intros [q ->] [q' Hq]; destruct Hne.
    by rewrite !list_encode_app !assoc in Hq; apply list_encode_suffix_eq in Hq.
57
  Qed.
58 59 60 61

  Lemma ndisj_subseteq_difference N1 N2 E :
    N1  N2  nclose N1  E  nclose N1  E  nclose N2.
  Proof. intros ?%ndisj_disjoint. set_solver. Qed.
62 63 64
End ndisjoint.

(* The hope is that registering these will suffice to solve most goals
65 66
of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *)
Hint Resolve ndisj_subseteq_difference : ndisj.
67
Hint Extern 0 (_  _) => apply ndot_ne_disjoint; congruence : ndisj.
68 69
Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj.
70 71

Ltac solve_ndisj := eauto with ndisj.