invariants.v 4.91 KB
Newer Older
1
Require Export algebra.base prelude.countable prelude.co_pset.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import program_logic.ownership.
Ralf Jung's avatar
Ralf Jung committed
3
Require Export program_logic.pviewshifts program_logic.weakestpre.
Ralf Jung's avatar
Ralf Jung committed
4
5
6
7
8
9
Import uPred.

Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
Local Hint Extern 99 ({[ _ ]}  _) => apply elem_of_subseteq_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12

Definition namespace := list positive.
Definition nnil : namespace := nil.
13
14
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
  encode x :: N.
Ralf Jung's avatar
Ralf Jung committed
15
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17

Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
18
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
21
Lemma encode_nclose N : encode N  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
23
Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
Proof.
  intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
26
  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
  by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
Qed.
29
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
31
32
Lemma nclose_disjoint `{Countable A} N (x y : A) :
  x  y  nclose (ndot N x)  nclose (ndot N y) = .
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
39
40
Proof.
  intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot.
  rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
  apply Hxy, (injective encode), (injective encode_nat); revert Hq.
  rewrite !(list_encode_cons (encode _)).
  rewrite !(associative_L _) (injective_iff (++ _)%positive) /=.
  generalize (encode_nat (encode y)).
  induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
41
42
Qed.

Ralf Jung's avatar
Ralf Jung committed
43
44
Local Hint Resolve nclose_subseteq ndot_nclose.

45
46
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
47
  ( i : positive, (i  nclose N)  ownI i P)%I.
Ralf Jung's avatar
Ralf Jung committed
48
49
50
51
52
53
54
55
56
57

Section inv.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.

Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof.
  intros n ? ? EQ. apply exists_ne=>i.
58
  apply and_ne; first done.
Ralf Jung's avatar
Ralf Jung committed
59
60
61
62
63
64
65
66
67
68
69
70
71
  by apply ownI_contractive.
Qed.

Global Instance inv_always_stable N P : AlwaysStable (inv N P) := _.

Lemma always_inv N P : ( inv N P)%I  inv N P.
Proof. by rewrite always_always. Qed.

(* We actually pretty much lose the abolity to deal with mask-changing view
   shifts when using `inv`. This is because we cannot exactly name the invariants
   any more. But that's okay; all this means is that sugar like the atomic
   triples will have to prove its own version of the open_close rule
   by unfolding `inv`. *)
Ralf Jung's avatar
Ralf Jung committed
72
(* TODO Can we prove something that helps for both open_close lemmas? *)
Ralf Jung's avatar
Ralf Jung committed
73
74
75
76
77
78
79
Lemma pvs_open_close E N P Q R :
  nclose N  E 
  P  (inv N R  (R - pvs (E  nclose N) (E  nclose N) (R  Q)))%I 
  P  pvs E E Q.
Proof.
  move=>HN -> {P}.
  rewrite /inv and_exist_r. apply exist_elim=>i.
80
  rewrite -associative. apply const_elim_l=>HiN.
Ralf Jung's avatar
Ralf Jung committed
81
  rewrite -(pvs_trans3 E (E  {[encode i]})) //; last by solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
82
  (* Add this to the local context, so that solve_elem_of finds it. *)
83
  assert ({[encode i]}  nclose N) by eauto.
Ralf Jung's avatar
Ralf Jung committed
84
85
  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
  rewrite {1}pvs_openI !pvs_frame_r.
Ralf Jung's avatar
Ralf Jung committed
86
  apply pvs_mask_frame_mono ; [solve_elem_of..|].
Ralf Jung's avatar
Ralf Jung committed
87
88
89
90
91
92
  rewrite (commutative _ (R)%I) -associative wand_elim_r pvs_frame_l.
  apply pvs_mask_frame_mono; [solve_elem_of..|].
  rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
  apply pvs_mask_frame'; solve_elem_of.
Qed.

Ralf Jung's avatar
Ralf Jung committed
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
Lemma wp_open_close E e N P (Q : val Λ  iProp Λ Σ) R :
  atomic e  nclose N  E 
  P  (inv N R  (R - wp (E  nclose N) e (λ v, R  Q v)))%I 
  P  wp E e Q.
Proof.
  move=>He HN -> {P}.
  rewrite /inv and_exist_r. apply exist_elim=>i.
  rewrite -associative. apply const_elim_l=>HiN.
  rewrite -(wp_atomic E (E  {[encode i]})) //; last by solve_elem_of+.
  (* Add this to the local context, so that solve_elem_of finds it. *)
  assert ({[encode i]}  nclose N) by eauto.
  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
  rewrite {1}pvs_openI !pvs_frame_r.
  apply pvs_mask_frame_mono; [solve_elem_of..|].
  rewrite (commutative _ (R)%I) -associative wand_elim_r wp_frame_l.
  apply wp_mask_frame_mono; [solve_elem_of..|]=>v.
  rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
  apply pvs_mask_frame'; solve_elem_of.
Qed.

Ralf Jung's avatar
Ralf Jung committed
113
114
Lemma pvs_alloc N P :  P  pvs N N (inv N P).
Proof.
115
  rewrite /inv (pvs_allocI N); first done.
Ralf Jung's avatar
Ralf Jung committed
116
117
  apply coPset_suffixes_infinite.
Qed.
Ralf Jung's avatar
Ralf Jung committed
118
119

End inv.