invariants.v 2.88 KB
Newer Older
1 2
From algebra Require Export base.
From program_logic Require Import ownership.
3
From program_logic Require Export namespaces pviewshifts weakestpre.
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
15 16

Section inv.
17
Context {Λ : language} {Σ : rFunctor}.
Ralf Jung's avatar
Ralf Jung committed
18 19 20
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
21
Implicit Types Φ : val Λ  iProp Λ Σ.
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
25

26 27
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Proof. rewrite /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
28 29 30 31

Lemma always_inv N P : ( inv N P)%I  inv N P.
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
  R  inv N P 
36 37
  R  ( P - fsa (E  nclose N) (λ a,  P  Ψ a)) 
  R  fsa E Ψ.
Ralf Jung's avatar
Ralf Jung committed
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 _ _)).
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
53 54
Qed.

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

57
Lemma pvs_open_close E N P Q R :
58
  nclose N  E 
59
  R  inv N P 
60
  R  ( P - pvs (E  nclose N) (E  nclose N) ( P  Q)) 
61
  R  (|={E}=> Q).
Ralf Jung's avatar
Ralf Jung committed
62
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
63

64
Lemma wp_open_close E e N P Φ R :
Ralf Jung's avatar
Ralf Jung committed
65
  atomic e  nclose N  E 
66
  R  inv N P 
Ralf Jung's avatar
Ralf Jung committed
67 68
  R  ( P - #> e @ E  nclose N {{ λ v,  P  Φ v }}) 
  R  #> e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
69
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Ralf Jung's avatar
Ralf Jung committed
70

71 72 73 74 75
Lemma inv_alloc N E P : nclose N  E   P  pvs E E (inv N P).
Proof. 
  intros. rewrite -(pvs_mask_weaken N) //.
  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
Qed.
Ralf Jung's avatar
Ralf Jung committed
76 77

End inv.