invariants.v 3.77 KB
Newer Older
1 2 3
From iris.algebra Require Export base.
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export namespaces pviewshifts weakestpre.
4
Import uPred.
5 6 7
Local Hint Extern 100 (@eq coPset _ _) => set_solver.
Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
Local Hint Extern 100 (_  _) => set_solver.
8
Local Hint Extern 99 ({[ _ ]}  _) => apply elem_of_subseteq_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10 11
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
12 13 14
  ( i,  (i  nclose N)  ownI i P)%I.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
15 16

Section inv.
17
Context {Λ : language} {Σ : iFunctor}.
18 19 20
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
21
Implicit Types Φ : val Λ  iProp Λ Σ.
22 23

Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Ralf Jung's avatar
Ralf Jung committed
24
Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
25

26
Global Instance inv_persistent N P : PersistentP (inv N P).
27
Proof. rewrite /inv; apply _. Qed.
28

29
Lemma always_inv N P : ( inv N P)  inv N P.
30 31
Proof. by rewrite always_always. Qed.

32
(** Invariants can be opened around any frame-shifting assertion. *)
33 34
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
  fsaV  nclose N  E 
35 36 37
  R  inv N P 
  R  ( P - fsa (E  nclose N) (λ a,  P  Ψ a)) 
  R  fsa E Ψ.
38
Proof.
39 40
  intros ? HN Hinv Hinner.
  rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
41
  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
42
  rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
43 44
  rewrite -(fsa_open_close E (E  {[encode i]})) //; last by set_solver+.
  (* Add this to the local context, so that set_solver finds it. *)
45
  assert ({[encode i]}  nclose N) by eauto.
46
  rewrite (always_sep_dup (ownI _ _)).
47
  rewrite {1}pvs_openI !pvs_frame_r.
48
  apply pvs_mask_frame_mono; [set_solver..|].
49
  rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
50
  apply fsa_mask_frame_mono; [set_solver..|]. intros a.
51
  rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
52
  apply pvs_mask_frame'; set_solver.
53
Qed.
54 55 56 57 58 59 60 61 62 63 64
Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
    `{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
  fsaV  nclose N  E 
  R  inv N P 
  R  (P - fsa (E  nclose N) (λ a,  P  Ψ a)) 
  R  fsa E Ψ.
Proof.
  intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
  trans (|={E  N}=> P  R)%I; first by rewrite pvs_timeless pvs_frame_r.
  apply (fsa_strip_pvs _). by rewrite HR wand_elim_r.
Qed.
65

66 67
(* Derive the concrete forms for pvs and wp, because they are useful. *)

68
Lemma pvs_inv E N P Q R :
69
  nclose N  E 
70 71 72
  R  inv N P 
  R  ( P - |={E  nclose N}=> ( P  Q)) 
  R  (|={E}=> Q).
Ralf Jung's avatar
Ralf Jung committed
73
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
74 75 76 77 78 79
Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
  nclose N  E 
  R  inv N P 
  R  (P - |={E  nclose N}=> ( P  Q)) 
  R  (|={E}=> Q).
Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
80

81
Lemma wp_inv E e N P Φ R :
Ralf Jung's avatar
Ralf Jung committed
82
  atomic e  nclose N  E 
83
  R  inv N P 
84 85
  R  ( P - WP e @ E  nclose N {{ λ v,  P  Φ v }}) 
  R  WP e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
86
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
87 88 89 90 91 92
Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
  atomic e  nclose N  E 
  R  inv N P 
  R  (P - WP e @ E  nclose N {{ λ v,  P  Φ v }}) 
  R  WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
Ralf Jung's avatar
Ralf Jung committed
93

94
Lemma inv_alloc N E P : nclose N  E   P  |={E}=> inv N P.
95
Proof.
96 97 98
  intros. rewrite -(pvs_mask_weaken N) //.
  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
Qed.
99
End inv.