namespaces.v 3.78 KB
Newer Older
1
From iris.prelude Require Export countable coPset.
2
From iris.algebra Require Export base.
3
Set Default Proof Using "Type".
4 5

Definition namespace := list positive.
6
Instance namespace_eq_dec : EqDecision namespace := _.
7 8 9
Instance namespace_countable : Countable namespace := _.
Typeclasses Opaque namespace.

10
Definition nroot : namespace := nil.
11 12

Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
13
  encode x :: N.
14 15 16 17 18 19
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.
20
Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux.
21
Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
22

23 24
Notation "N .@ x" := (ndot N x)
  (at level 19, left associativity, format "N .@ x") : C_scope.
Ralf Jung's avatar
Ralf Jung committed
25
Notation "(.@)" := ndot (only parsing) : C_scope.
Ralf Jung's avatar
Ralf Jung committed
26

27
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1  nclose N2.
28

29
Section namespace.
30 31
  Context `{Countable A}.
  Implicit Types x y : A.
32 33
  Implicit Types N : namespace.
  Implicit Types E : coPset.
34

35 36 37
  Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
  Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.

38
  Lemma nclose_nroot : nroot = .
39
  Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
40
  Lemma encode_nclose N : encode N  N.
41 42 43 44 45
  Proof.
    rewrite nclose_eq.
    by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
  Qed.

46
  Lemma nclose_subseteq N x : N.@x  (N : coPset).
47 48 49 50 51 52
  Proof.
    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]. }
    by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
  Qed.
53

54
  Lemma nclose_subseteq' E N x : N  E  N.@x  E.
55 56
  Proof. intros. etrans; eauto using nclose_subseteq. Qed.

57
  Lemma ndot_nclose N x : encode (N.@x)   N.
58
  Proof. apply nclose_subseteq with x, encode_nclose. Qed.
59
  Lemma nclose_infinite N : ¬set_finite ( N : coPset).
60 61
  Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.

62
  Lemma ndot_ne_disjoint N x y : x  y  N.@x  N.@y.
63
  Proof.
64
    intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
65 66
    intros [qx ->] [qy Hqy].
    revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
67 68
  Qed.

69
  Lemma ndot_preserve_disjoint_l N E x : N  E  N.@x  E.
70
  Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
71

72
  Lemma ndot_preserve_disjoint_r N E x : E  N  E  N.@x.
73
  Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
74

75
  Lemma ndisj_subseteq_difference N E F : E  N  E  F  E  F  N.
76
  Proof. set_solver. Qed.
77 78 79 80 81 82

  Lemma namespace_subseteq_difference_l E1 E2 E3 : E1  E3  E1  E2  E3.
  Proof. set_solver. Qed.

  Lemma ndisj_difference_l E N1 N2 : N2  (N1 : coPset)  E  N1  N2.
  Proof. set_solver. Qed.
83
End namespace.
84 85

(* The hope is that registering these will suffice to solve most goals
86 87 88 89
of the forms:
- [N1 ⊥ N2] 
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
90
Hint Resolve ndisj_subseteq_difference : ndisj.
91
Hint Extern 0 (_  _) => apply ndot_ne_disjoint; congruence : ndisj.
92 93
Hint Extern 1 (_  _) => apply ndot_preserve_disjoint_l : ndisj.
Hint Extern 1 (_  _) => apply ndot_preserve_disjoint_r : ndisj.
94
Hint Extern 1 (_  _) => apply nclose_subseteq' : ndisj.
95
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
96
Hint Resolve ndisj_difference_l : ndisj.
97

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