invariants.v 2.83 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 5 6 7 8
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
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 17 18 19 20 21 22

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

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

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

31
(** Invariants can be opened around any frame-shifting assertion. *)
32 33 34
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}
    E N P (Q : A  iProp Λ Σ) R :
  fsaV 
Ralf Jung's avatar
Ralf Jung committed
35
  nclose N  E 
36
  R  inv N P 
37 38
  R  ( P - fsa (E  nclose N) (λ a,  P  Q a)) 
  R  fsa E Q.
Ralf Jung's avatar
Ralf Jung committed
39
Proof.
40 41
  intros ? HN Hinv Hinner.
  rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
42
  rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
43
  rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
44
  rewrite -(fsa_open_close E (E  {[encode i]})) //; last by solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
45
  (* Add this to the local context, so that solve_elem_of finds it. *)
46
  assert ({[encode i]}  nclose N) by eauto.
47
  rewrite (always_sep_dup (ownI _ _)).
Ralf Jung's avatar
Ralf Jung committed
48
  rewrite {1}pvs_openI !pvs_frame_r.
49
  apply pvs_mask_frame_mono; [solve_elem_of..|].
50
  rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
51
  apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
52
  rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
Ralf Jung's avatar
Ralf Jung committed
53 54 55
  apply pvs_mask_frame'; solve_elem_of.
Qed.

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

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

65
Lemma wp_open_close E e N P (Q : val Λ  iProp Λ Σ) R :
Ralf Jung's avatar
Ralf Jung committed
66
  atomic e  nclose N  E 
67
  R  inv N P 
68
  R  ( P - wp (E  nclose N) e (λ v, P  Q v)) 
69
  R  wp E e Q.
Ralf Jung's avatar
Ralf Jung committed
70
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Ralf Jung's avatar
Ralf Jung committed
71

72
Lemma inv_alloc N P :  P  pvs N N (inv N P).
73
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
Ralf Jung's avatar
Ralf Jung committed
74 75

End inv.