namespaces.v 3.09 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
Instance namespace_eq_dec : EqDecision namespace := _.
6 7 8
Instance namespace_countable : Countable namespace := _.
Typeclasses Opaque namespace.

9
Definition nroot : namespace := nil.
10 11

Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
12
  encode x :: N.
13 14 15 16 17 18 19 20
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.
21

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

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

46
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1  nclose N2.
47 48 49 50 51

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

52
  Lemma ndot_ne_disjoint N x y : x  y  N .@ x  N .@ y.
53
  Proof.
54
    intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
55 56
    intros [qx ->] [qy Hqy].
    revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
57 58
  Qed.

59 60
  Lemma ndot_preserve_disjoint_l N E x : nclose N  E  nclose (N .@ x)  E.
  Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
61

62 63
  Lemma ndot_preserve_disjoint_r N E x : E  nclose N  E  nclose (N .@ x).
  Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
64

65 66 67
  Lemma ndisj_subseteq_difference N E F :
    E  nclose N  E  F  E  F  nclose N.
  Proof. set_solver. Qed.
68 69 70
End ndisjoint.

(* The hope is that registering these will suffice to solve most goals
Robbert Krebbers's avatar
Robbert Krebbers committed
71
of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *)
72
Hint Resolve ndisj_subseteq_difference : ndisj.
73
Hint Extern 0 (_  _) => apply ndot_ne_disjoint; congruence : ndisj.
74 75
Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj.
76

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