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

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

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

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

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

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).
59
Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
60

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

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 
Ralf Jung's avatar
Ralf Jung committed
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 80
  rewrite /inv sep_exist_r. apply exist_elim=>i.
  rewrite always_and_sep_l' -associative. apply const_elim_sep_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
  rewrite (always_sep_dup' (ownI _ _)).
Ralf Jung's avatar
Ralf Jung committed
85
  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 
Ralf Jung's avatar
Ralf Jung committed
95
  (inv N P  (P - wp (E  nclose N) e (λ v, P  Q v)))  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
  rewrite /inv sep_exist_r. apply exist_elim=>i.
  rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN.
Ralf Jung's avatar
Ralf Jung committed
100 101 102
  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.
Ralf Jung's avatar
Ralf Jung committed
103
  rewrite (always_sep_dup' (ownI _ _)).
Ralf Jung's avatar
Ralf Jung committed
104 105
  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.

112
Lemma inv_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.