cancelable_invariants.v 4.76 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.base_logic.lib Require Export invariants.
2
From iris.bi.lib Require Import fractional.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.algebra Require Export frac.
4
From iris.proofmode Require Import tactics.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8
Import uPred.

Class cinvG Σ := cinv_inG :> inG Σ fracR.
9 10 11 12
Definition cinvΣ : gFunctors := #[GFunctor fracR].

Instance subG_cinvΣ {Σ} : subG cinvΣ Σ  cinvG Σ.
Proof. solve_inG. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14

Section defs.
15
  Context `{!invG Σ, !cinvG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18 19

  Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.

  Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ :=
20
    ( P',   (P  P')  inv N (P'  cinv_own γ 1%Qp))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
End defs.

23
Instance: Params (@cinv) 5 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25

Section proofs.
26
  Context `{!invG Σ, !cinvG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28
  Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
  Proof. rewrite /cinv_own; apply _. Qed.

31 32
  Global Instance cinv_contractive N γ : Contractive (cinv N γ).
  Proof. solve_contractive. Qed.
33
  Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
34
  Proof. exact: contractive_ne. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  Global Instance cinv_proper N γ : Proper (() ==> ()) (cinv N γ).
36
  Proof. exact: ne_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
  Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
  Proof. rewrite /cinv; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
41
  Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
42
  Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Global Instance cinv_own_as_fractional γ q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
44
    AsFractional (cinv_own γ q) (cinv_own γ) q.
45
  Proof. split. done. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47 48
  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 - cinv_own γ q2 -  (q1 + q2)%Qp.
  Proof. apply (own_valid_2 γ q1 q2). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50 51 52 53 54
  Lemma cinv_own_1_l γ q : cinv_own γ 1 - cinv_own γ q - False.
  Proof.
    iIntros "H1 H2".
    iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55

56 57 58 59
  Lemma cinv_iff N γ P P' :
      (P  P') - cinv N γ P - cinv N γ P'.
  Proof.
    iIntros "#HP' Hinv". iDestruct "Hinv" as (P'') "[#HP'' Hinv]".
60
    iExists _. iFrame "Hinv". iAlways. iNext. iSplit.
61 62 63 64
    - iIntros "?". iApply "HP''". iApply "HP'". done.
    - iIntros "?". iApply "HP'". iApply "HP''". done.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
65 66 67
  Lemma cinv_alloc_strong (I : gname  Prop) E N :
    pred_infinite I 
    (|={E}=>  γ,  I γ   cinv_own γ 1   P,  P ={E}= cinv N γ P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Proof.
Dan Frumin's avatar
Dan Frumin committed
69
    iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
70
    iExists γ; iIntros "!> {$Hγ $Hfresh}" (P) "HP".
71
    iMod (inv_alloc N _ (P  own γ 1%Qp)%I with "[HP]"); first by eauto.
72 73 74
    iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
75 76 77 78 79 80 81
  Lemma cinv_alloc_cofinite (G : gset gname) E N :
    (|={E}=>  γ,  γ  G   cinv_own γ 1   P,  P ={E}= cinv N γ P)%I.
  Proof.
    apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
    exists (fresh (G  E')). apply not_elem_of_union, is_fresh.
  Qed.

82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
  Lemma cinv_open_strong E N γ p P :
    N  E 
    cinv N γ P - cinv_own γ p ={E,E∖↑N}=
     P  cinv_own γ p  ( P  cinv_own γ 1 ={E∖↑N,E}= True).
  Proof.
    iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
    iInv N as "[HP | >Hγ']" "Hclose".
    - iIntros "!> {$Hγ}". iSplitL "HP".
      + iNext. iApply "HP'". done.
      + iIntros "[HP|Hγ]".
        * iApply "Hclose". iLeft. iNext. by iApply "HP'".
        * iApply "Hclose". iRight. by iNext.
    - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
  Qed.

97 98
  Lemma cinv_alloc E N P :  P ={E}=  γ, cinv N γ P  cinv_own γ 1.
  Proof.
Dan Frumin's avatar
Dan Frumin committed
99
    iIntros "HP". iMod (cinv_alloc_cofinite  E N) as (γ _) "[Hγ Halloc]".
100
    iExists γ. iFrame "Hγ". by iApply "Halloc".
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102
  Qed.

103
  Lemma cinv_cancel E N γ P : N  E  cinv N γ P - cinv_own γ 1 ={E}=  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Proof.
105 106 107
    iIntros (?) "#Hinv Hγ".
    iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
    iApply "H". by iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109 110
  Qed.

  Lemma cinv_open E N γ p P :
111
    N  E 
112
    cinv N γ P - cinv_own γ p ={E,E∖↑N}=  P  cinv_own γ p  ( P ={E∖↑N,E}= True).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  Proof.
114 115 116
    iIntros (?) "#Hinv Hγ".
    iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
    iIntros "!> HP". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
118

119
  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
Ralf Jung's avatar
Ralf Jung committed
120

121
  Global Instance into_acc_cinv E N γ P p :
122
    IntoAcc (X:=unit) (cinv N γ P)
123
            (N  E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
124
            (λ _,  P  cinv_own γ p)%I (λ _,  P)%I (λ _, None)%I.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
125
  Proof.
126 127
    rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
    rewrite exist_unit -assoc.
Ralf Jung's avatar
Ralf Jung committed
128
    iApply (cinv_open with "Hinv"); done.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
129
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
End proofs.
131 132

Typeclasses Opaque cinv_own cinv.