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

Definition namespace := list positive.
5
Definition nroot : namespace := nil.
6 7

Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
8
  encode x :: N.
9 10 11 12 13 14 15 16
Definition ndot_aux : { x | x = @ndot_def }. by eexists. Qed.
Definition ndot {A A_dec A_count}:= proj1_sig ndot_aux A A_dec A_count.
Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux.

Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed.
Coercion nclose := proj1_sig nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
17

Ralf Jung's avatar
Ralf Jung committed
18 19
Infix ".@" := ndot (at level 19, left associativity) : C_scope.
Notation "(.@)" := ndot (only parsing) : C_scope.
Ralf Jung's avatar
Ralf Jung committed
20

21
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
22
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
23
Lemma nclose_nroot : nclose nroot = .
24
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
25
Lemma encode_nclose N : encode N  nclose N.
26 27 28 29
Proof.
  rewrite nclose_eq.
  by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Ralf Jung's avatar
Ralf Jung committed
30
Lemma nclose_subseteq `{Countable A} N x : nclose (N .@ x)  nclose N.
31
Proof.
32 33 34
  intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
  intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
  { by exists [encode x]. }
35 36
  by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Ralf Jung's avatar
Ralf Jung committed
37
Lemma ndot_nclose `{Countable A} N x : encode (N .@ x)  nclose N.
38
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
39 40
Lemma nclose_infinite N : ¬set_finite (nclose N).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
41 42 43 44

Instance ndisjoint : Disjoint namespace := λ N1 N2,
   N1' N2', N1' `suffix_of` N1  N2' `suffix_of` N2 
             length N1' = length N2'  N1'  N2'.
45
Typeclasses Opaque ndisjoint.
46 47 48 49 50

Section ndisjoint.
  Context `{Countable A}.
  Implicit Types x y : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
51
  Global Instance ndisjoint_symmetric : Symmetric ndisjoint.
52 53
  Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.

54
  Lemma ndot_ne_disjoint N x y : x  y  N .@ x  N .@ y.
55
  Proof. intros. exists (N .@ x), (N .@ y); rewrite ndot_eq; naive_solver. Qed.
56

Ralf Jung's avatar
Ralf Jung committed
57
  Lemma ndot_preserve_disjoint_l N1 N2 x : N1  N2  N1 .@ x  N2.
58 59
  Proof.
    intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
60
    split_and?; try done; []. rewrite ndot_eq. by apply suffix_of_cons_r.
61 62
  Qed.

Ralf Jung's avatar
Ralf Jung committed
63
  Lemma ndot_preserve_disjoint_r N1 N2 x : N1  N2  N1  N2 .@ x .
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
65

Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Lemma ndisj_disjoint N1 N2 : N1  N2  nclose N1  nclose N2.
67
  Proof.
68 69
    intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne) p.
    rewrite nclose_eq /nclose.
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
    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.
72
  Qed.
73 74 75 76

  Lemma ndisj_subseteq_difference N1 N2 E :
    N1  N2  nclose N1  E  nclose N1  E  nclose N2.
  Proof. intros ?%ndisj_disjoint. set_solver. Qed.
77 78 79
End ndisjoint.

(* The hope is that registering these will suffice to solve most goals
Robbert Krebbers's avatar
Robbert Krebbers committed
80
of the form [N1  N2] and those of the form [N1  E  N2  ..  Nn]. *)
81
Hint Resolve ndisj_subseteq_difference : ndisj.
82
Hint Extern 0 (_  _) => apply ndot_ne_disjoint; congruence : ndisj.
83 84
Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj.
85

86
Ltac solve_ndisj := solve [eauto with ndisj].