invariants.v 2.58 KB
Newer Older
1
From iris.program_logic Require Import ownership.
2
From iris.program_logic Require Export namespaces.
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
(** Derived forms and lemmas about them. *)
7
Definition inv_def {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
8
  ( i,  (i  nclose N)  ownI i P)%I.
9 10 11
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Λ Σ} := proj1_sig inv_aux Λ Σ.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
12 13
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
14 15

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

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

27
Global Instance inv_persistent N P : PersistentP (inv N P).
28
Proof. rewrite inv_eq /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
29

Robbert Krebbers's avatar
Robbert Krebbers committed
30
Lemma always_inv N P :  inv N P  inv N P.
Ralf Jung's avatar
Ralf Jung committed
31 32
Proof. by rewrite always_always. Qed.

33
Lemma inv_alloc N E P : nclose N  E   P ={E}=> inv N P.
34
Proof.
35
  intros. rewrite -(pvs_mask_weaken N) //.
36
  by rewrite inv_eq /inv (pvs_allocI N); last apply nclose_infinite.
37
Qed.
38

39 40 41
(** Fairly explicit form of opening invariants *)
Lemma inv_open E N P :
  nclose N  E 
42
  inv N P   E',  (E  nclose N  E'  E) 
43 44
                    |={E,E'}=>  P  ( P ={E',E}= True).
Proof.
45
  rewrite inv_eq /inv. iDestruct 1 as (i) "[% #Hi]".
46 47 48 49
  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|].
50
  done.
51 52 53 54
Qed.

(** Invariants can be opened around any frame-shifting assertion. This is less
    verbose to apply than [inv_open]. *)
55 56
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
  fsaV  nclose N  E 
57
  inv N P  ( P - fsa (E  nclose N) (λ a,  P  Ψ a))  fsa E Ψ.
58
Proof.
59 60
  iIntros (??) "[Hinv HΨ]".
  iDestruct (inv_open E N P with "Hinv") as (E') "[% Hvs]"; first done.
61
  iApply (fsa_open_close E E'); auto; first set_solver.
62
  iPvs "Hvs" as "[HP Hvs]"; first set_solver.
63 64
  (* TODO: How do I do sth. like [iSpecialize "HΨ HP"]? *)
  iPvsIntro. iApply (fsa_mask_weaken _ (E  N)); first set_solver.
65
  iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ"; simpl.
66
  iIntros (v) "[HP HΨ]". by iPvs ("Hvs" with "HP"); first set_solver.
67
Qed.
Ralf Jung's avatar
Ralf Jung committed
68
End inv.