invariants.v 4.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.base_logic.lib Require Export fancy_updates.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
2
From stdpp Require Export namespaces.
3
From iris.base_logic.lib Require Import wsat.
4
From iris.algebra Require Import gmap.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
5
From iris.proofmode Require Import tactics.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
(** Derived forms and lemmas about them. *)
10
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
11
  ( i P', i  (N:coPset)    (P'  P)  ownI i P')%I.
12
Definition inv_aux : seal (@inv_def). by eexists. Qed.
13 14
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
15
Instance: Params (@inv) 3.
16
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
17 18

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

24
Global Instance inv_contractive N : Contractive (inv N).
25
Proof. rewrite inv_eq. solve_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
26

27 28 29
Global Instance inv_ne N : NonExpansive (inv N).
Proof. apply contractive_ne, _. Qed.

30
Global Instance inv_proper N : Proper (() ==> ()) (inv N).
31 32
Proof. apply ne_proper, _. Qed.

33
Global Instance inv_persistent N P : Persistent (inv N P).
34
Proof. rewrite inv_eq /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
35

36 37 38 39 40 41 42 43
Lemma inv_iff N P Q :   (P  Q) - inv N P - inv N Q.
Proof.
  iIntros "#HPQ". rewrite inv_eq. iDestruct 1 as (i P') "(?&#HP&?)".
  iExists i, P'. iFrame. iNext; iAlways; iSplit.
  - iIntros "HP'". iApply "HPQ". by iApply "HP".
  - iIntros "HQ". iApply "HP". by iApply "HPQ".
Qed.

44
Lemma fresh_inv_name (E : gset positive) N :  i, i  E  i  (N:coPset).
45 46 47 48 49 50 51 52
Proof.
  exists (coPpick ( N  coPset.of_gset E)).
  rewrite -coPset.elem_of_of_gset (comm and) -elem_of_difference.
  apply coPpick_elem_of=> Hfin.
  eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
  apply of_gset_finite.
Qed.

53
Lemma inv_alloc N E P :  P ={E}= inv N P.
54
Proof.
55
  rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
56
  iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
57
    as (i ?) "[$ ?]"; auto using fresh_inv_name.
58
  do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto.
59
Qed.
60

61
Lemma inv_alloc_open N E P :
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  N  E  (|={E, E∖↑N}=> inv N P  (P ={E∖↑N, E}= True))%I.
63
Proof.
64
  rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
65
  iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
66
    as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
67 68 69 70 71
  iAssert (ownE {[i]}  ownE ( N  {[i]})  ownE (E   N))%I
    with "[HE]" as "(HEi & HEN\i & HE\N)".
  { rewrite -?ownE_op; [|set_solver..].
    rewrite assoc_L -!union_difference_L //. set_solver. }
  do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
72
  iSplitL "Hi".
73
  { iExists i, P. rewrite -(iff_refl True%I). auto. }
74
  iIntros "HP [Hw HE\N]".
75 76
  iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
  do 2 iModIntro. iSplitL; [|done].
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  iCombine "HEi HEN\i HE\N" as "HEN".
78
  rewrite -?ownE_op; [|set_solver..].
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  rewrite assoc_L -!union_difference_L //; set_solver.
80 81
Qed.

82
Lemma inv_open E N P :
83
  N  E  inv N P ={E,E∖↑N}=  P  ( P ={E∖↑N,E}= True).
84
Proof.
85
  rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def.
86
  iDestruct 1 as (i P') "(Hi & #HP' & #HiP)".
87
  iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
88 89
  rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
  rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
90
  iIntros "(Hw & [HE $] & $) !> !>".
91 92 93 94
  iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & HP & HD)".
  iDestruct ("HP'" with "HP") as "$".
  iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP".
  iApply "HP'". iFrame.
95 96
Qed.

97
Lemma inv_open_strong E N P :
98
  N  E  inv N P ={E,E∖↑N}=  P   E',  P ={E',N  E'}= True.
99 100 101 102 103 104
Proof.
  iIntros (?) "Hinv".
  iPoseProof (inv_open ( N) N P with "Hinv") as "H"; first done.
  rewrite difference_diag_L.
  iPoseProof (fupd_mask_frame_r _ _ (E   N) with "H") as "H"; first set_solver.
  rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
105 106 107
  iIntros (E') "HP". iSpecialize ("H" with "HP").
  iPoseProof (fupd_mask_frame_r _ _ E' with "H") as "H"; first set_solver.
  by rewrite left_id_L.
108 109
Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
110 111
Global Instance into_inv_inv N P : IntoInv (inv N P) N.

112
Global Instance elim_inv_inv E N P Q Q' :
Ralf Jung's avatar
Ralf Jung committed
113 114
  InvOpener E (E∖↑N) ( P) ( P) None Q Q' 
  ElimInv (N  E) (inv N P) True ( P) Q Q'.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
115
Proof.
Ralf Jung's avatar
Ralf Jung committed
116 117
  rewrite /ElimInv /InvOpener. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
  iApply (Hopener with "Hcont"). iApply inv_open; done.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
118 119
Qed.

120
Lemma inv_open_timeless E N P `{!Timeless P} :
121
  N  E  inv N P ={E,E∖↑N}= P  (P ={E∖↑N,E}= True).
122
Proof.
123 124
  iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!> {$HP} HP". iApply "Hclose"; auto.
125
Qed.
Ralf Jung's avatar
Ralf Jung committed
126
End inv.