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

8
(** Derived forms and lemmas about them. *)
9
Definition inv_def `{irisG Λ Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
10
  ( i,  (i  nclose N)  ownI i P)%I.
11
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
12
Definition inv {Λ Σ i} := proj1_sig inv_aux Λ Σ i.
13
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
14
Instance: Params (@inv) 4.
15
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
16 17

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

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

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

32
Lemma inv_alloc N E P :  P ={E}=> inv N P.
33
Proof.
34 35 36 37 38 39 40 41 42
  rewrite inv_eq /inv_def pvs_eq /pvs_def. iIntros "HP [Hw $]".
  iVs (ownI_alloc ( nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
  - intros Ef. exists (coPpick (nclose N  coPset.of_gset Ef)).
    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
    apply coPpick_elem_of=> Hfin.
    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
    apply of_gset_finite.
  - by iFrame.
  - rewrite /uPred_now_True; eauto.
43
Qed.
44

45
Lemma inv_open E N P :
46
  nclose N  E  inv N P ={E,EN}=>  P  ( P ={EN,E}= True).
47
Proof.
48 49 50 51 52 53
  rewrite inv_eq /inv_def pvs_eq /pvs_def; iDestruct 1 as (i) "[Hi #HiP]".
  iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
  rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
  rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
  iIntros "(Hw & [HE $] & $)"; iVsIntro; iRight.
  iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  iIntros "HP [Hw $] !==>"; iRight. iApply ownI_close; by iFrame.
55 56
Qed.

57 58
Lemma inv_open_timeless E N P `{!TimelessP P} :
  nclose N  E  inv N P ={E,EN}=> P  (P ={EN,E}= True).
59
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
  iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
62
Qed.
Ralf Jung's avatar
Ralf Jung committed
63
End inv.