invariants.v 2.46 KB
Newer Older
1
From iris.program_logic Require Import ownership.
2
From iris.program_logic Require Export namespaces lviewshifts.
3
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 46 47 48 49
(** Fairly explicit form of opening invariants *)
Lemma inv_open E N P :
  nclose N  E 
  inv N P   E',  (E  nclose N  E'  E'  E) 
                    |={E,E'}=>  P  ( P ={E',E}= True).
Proof.
  rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]".
  iExists (E  {[ i ]}). iSplit. { iPureIntro. set_solver. }
  iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
  iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
  iPvs (pvs_closeI' _ _ P with "[HP]"); [set_solver|iSplit; done|set_solver|].
  iPvsIntro. done.
Qed.

(** Invariants can be opened around any frame-shifting assertion. This is less
    verbose to apply than [inv_open]. *)
50 51 52 53
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.
54 55 56 57 58 59 60 61 62
  iIntros {??} "[Hinv HΨ]".
  iDestruct (inv_open E N P with "Hinv") as {E'} "[% Hvs]"; first done.
  iApply (fsa_open_close E E'); auto; first set_solver.
  iPvs "Hvs" as "[HP Hvs]";first set_solver.
  (* TODO: How do I do sth. like [iSpecialize "HΨ HP"]? *)
  iPvsIntro. iApply (fsa_mask_weaken _ (E  N)); first set_solver.
  iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ".
  simpl. iIntros {v} "[HP HΨ]". iPvs ("Hvs" with "HP"); first set_solver.
  by iPvsIntro.
63
Qed.
Ralf Jung's avatar
Ralf Jung committed
64
End inv.