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

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
12
Infix ".:" := ndot (at level 19, left associativity) : C_scope.
Notation "(.:)" := ndot : C_scope.

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
31
32
33
34
35
36
37
38
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'.

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.

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

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

Ralf Jung's avatar
Ralf Jung committed
48
  Lemma ndot_preserve_disjoint_r N1 N2 x : N1  N2  N1  N2 .: x .
49
50
51
52
53
54
55
56
57
58
  Proof. rewrite ![N1  _]comm. apply ndot_preserve_disjoint_l. Qed.

  Lemma ndisj_disjoint N1 N2 : N1  N2  nclose N1  nclose N2 = .
  Proof.
    intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne).
    apply elem_of_equiv_empty_L=> p; unfold nclose.
    rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
    rewrite !list_encode_app !assoc in Hq.
    by eapply Hne, list_encode_suffix_eq.
  Qed.
59
60
61
End ndisjoint.

(* This tactic solves goals about inclusion and disjointness
62
   of masks (i.e., coPsets) with set_solver, taking
63
64
65
66
67
68
   disjointness of namespaces into account. *)
(* TODO: This tactic is by far now yet as powerful as it should be.
   For example, given N1  N2, it should be able to solve
   nclose (ndot N1 x)  N2  . It should also solve
   (ndot N x)  (ndot N y)   if x  y is in the context or
   follows from [discriminate]. *)
69
Ltac set_solver_ndisj :=
70
71
72
73
  repeat match goal with
         (* TODO: Restrict these to have type namespace *)
         | [ H : (?N1  ?N2) |-_ ] => apply ndisj_disjoint in H
         end;
74
  set_solver.
75
(* TODO: restrict this to match only if this is  of coPset *)
76
Hint Extern 500 (_  _) => set_solver_ndisj : ndisj.
77
78
79
80
81
82
(* The hope is that registering these will suffice to solve most goals
   of the form N1  N2.
   TODO: Can this prove x  y if discriminate can? *)
Hint Resolve ndot_ne_disjoint : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj.