invariants.v 4.92 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
48
49
  ( i,  (i  nclose N)  ownI i P)%I.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
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).
58
Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
59

60
61
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Proof. rewrite /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
62
63
64
65

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

Ralf Jung's avatar
Ralf Jung committed
66
67
68
69
70
71
72
(* There is not really a way to provide versions of pvs_openI and pvs_closeI
   that work with inv. The issue is that these rules track the exact current
   mask too precisely. However, we *can* provide abstract rules by
   performing both the opening and the closing of the invariant in the rule,
   and then implicitly framing all the unused invariants around the
   "inner" view shift provided by the client. *)

73
Lemma pvs_open_close E N P Q :
Ralf Jung's avatar
Ralf Jung committed
74
  nclose N  E 
75
  (inv N P  (P - pvs (E  nclose N) (E  nclose N) (P  Q)))  pvs E E Q.
Ralf Jung's avatar
Ralf Jung committed
76
Proof.
77
  move=>HN.
Ralf Jung's avatar
Ralf Jung committed
78
  rewrite /inv and_exist_r. apply exist_elim=>i.
79
  rewrite -associative. apply const_elim_l=>HiN.
Ralf Jung's avatar
Ralf Jung committed
80
  rewrite -(pvs_trans3 E (E  {[encode i]})) //; last by solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
81
  (* Add this to the local context, so that solve_elem_of finds it. *)
82
  assert ({[encode i]}  nclose N) by eauto.
Ralf Jung's avatar
Ralf Jung committed
83
84
  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
  rewrite {1}pvs_openI !pvs_frame_r.
Ralf Jung's avatar
Ralf Jung committed
85
  apply pvs_mask_frame_mono ; [solve_elem_of..|].
86
  rewrite (commutative _ (_)%I) -associative wand_elim_r pvs_frame_l.
Ralf Jung's avatar
Ralf Jung committed
87
88
89
90
91
  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.

92
Lemma wp_open_close E e N P (Q : val Λ  iProp Λ Σ) :
Ralf Jung's avatar
Ralf Jung committed
93
  atomic e  nclose N  E 
94
  (inv N P  (P - wp (E  nclose N) e (λ v, P  Q v)))%I  wp E e Q.
Ralf Jung's avatar
Ralf Jung committed
95
Proof.
96
  move=>He HN.
Ralf Jung's avatar
Ralf Jung committed
97
98
99
100
101
102
103
104
  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..|].
105
  rewrite (commutative _ (_)%I) -associative wand_elim_r wp_frame_l.
Ralf Jung's avatar
Ralf Jung committed
106
107
108
109
110
  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
111
Lemma pvs_alloc N P :  P  pvs N N (inv N P).
112
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
Ralf Jung's avatar
Ralf Jung committed
113
114

End inv.