invariants.v 4.87 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
  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.

Ralf Jung's avatar
Ralf Jung committed
67 68 69 70 71 72 73
(* 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. *)

74
Lemma pvs_open_close E N P Q :
Ralf Jung's avatar
Ralf Jung committed
75
  nclose N  E 
76
  (inv N P  (P - pvs (E  nclose N) (E  nclose N) (P  Q)))  pvs E E Q.
Ralf Jung's avatar
Ralf Jung committed
77
Proof.
78
  move=>HN.
Ralf Jung's avatar
Ralf Jung committed
79
  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..|].
87
  rewrite (commutative _ (_)%I) -associative wand_elim_r pvs_frame_l.
Ralf Jung's avatar
Ralf Jung committed
88 89 90 91 92
  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.

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

End inv.