invariants.v 1.78 KB
Newer Older
1
From iris.program_logic Require Import ownership.
2 3
From iris.program_logic Require Export namespaces.
From iris.proofmode Require Import pviewshifts.
Ralf Jung's avatar
Ralf Jung committed
4
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6 7
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
8 9 10
  ( i,  (i  nclose N)  ownI i P)%I.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
11 12

Section inv.
13
Context {Λ : language} {Σ : iFunctor}.
Ralf Jung's avatar
Ralf Jung committed
14 15 16
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.
17
Implicit Types Φ : val Λ  iProp Λ Σ.
Ralf Jung's avatar
Ralf Jung committed
18 19

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

22
Global Instance inv_persistent N P : PersistentP (inv N P).
23
Proof. rewrite /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Lemma always_inv N P :  inv N P  inv N P.
Ralf Jung's avatar
Ralf Jung committed
26 27
Proof. by rewrite always_always. Qed.

28
Lemma inv_alloc N E P : nclose N  E   P  |={E}=> inv N P.
29
Proof.
30 31 32
  intros. rewrite -(pvs_mask_weaken N) //.
  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
Qed.
33 34 35 36 37 38 39 40 41 42 43 44 45

(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
  fsaV  nclose N  E 
  (inv N P  ( P - fsa (E  nclose N) (λ a,  P  Ψ a)))  fsa E Ψ.
Proof.
  iIntros {??} "[#Hinv HΨ]"; rewrite /inv; iDestruct "Hinv" as {i} "[% Hi]".
  iApply (fsa_open_close E (E  {[encode i]})); auto; first by set_solver.
  iPvs (pvs_openI' _ _ with "Hi") as "HP"; [set_solver..|iPvsIntro].
  iApply (fsa_mask_weaken _ (E  N)); first set_solver.
  iApply fsa_wand_r; iSplitL; [by iApply "HΨ"|iIntros {v} "[HP HΨ]"].
  iPvs (pvs_closeI' _ _ P with "[HP]"); [auto|by iSplit|set_solver|done].
Qed.
Ralf Jung's avatar
Ralf Jung committed
46
End inv.