cancelable_invariants.v 2.46 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.program_logic Require Export invariants.
From iris.algebra Require Export frac.
3
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
Import uPred.

Class cinvG Σ := cinv_inG :> inG Σ fracR.

Section defs.
  Context `{irisG Λ Σ, cinvG Σ}.

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

  Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ :=
    inv N (P  cinv_own γ 1%Qp)%I.
End defs.

Instance: Params (@cinv) 6.
Typeclasses Opaque cinv_own cinv.

Section proofs.
  Context `{irisG Λ Σ, cinvG Σ}.

  Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
  Proof. rewrite /cinv_own; apply _. Qed.

  Global Instance cinv_ne N γ n : Proper (dist n ==> dist n) (cinv N γ).
  Proof. solve_proper. Qed.
  Global Instance cinv_proper N γ : Proper (() ==> ()) (cinv N γ).
  Proof. apply (ne_proper _). Qed.

  Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
  Proof. rewrite /cinv; apply _. Qed.

  Lemma cinv_own_op γ q1 q2 :
    cinv_own γ q1  cinv_own γ q2  cinv_own γ (q1 + q2).
  Proof. by rewrite /cinv_own own_op. Qed.

  Lemma cinv_own_half γ q : cinv_own γ (q/2)  cinv_own γ (q/2)  cinv_own γ q.
  Proof. by rewrite cinv_own_op Qp_div_2. Qed.

  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1  cinv_own γ q2   (q1 + q2)%Qp.
42
  Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

  Lemma cinv_own_1_l γ q : cinv_own γ 1  cinv_own γ q  False.
  Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.

  Lemma cinv_alloc E N P :  P ={E}=>  γ, cinv N γ P  cinv_own γ 1.
  Proof.
    rewrite /cinv /cinv_own. iIntros "HP".
    iVs (own_alloc 1%Qp) as (γ) "H1"; first done.
    iVs (inv_alloc N _ (P  own γ 1%Qp)%I with "[HP]"); eauto.
  Qed.

  Lemma cinv_cancel E N γ P :
    nclose N  E  cinv N γ P  cinv_own γ 1 ={E}=  P.
  Proof.
    rewrite /cinv. iIntros (?) "#Hinv Hγ".
    iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
    iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
  Qed.

  Lemma cinv_open E N γ p P :
    nclose N  E 
    cinv N γ P  cinv_own γ p ={E,EN}=  P  cinv_own γ p  ( P ={EN,E}= True).
  Proof.
    rewrite /cinv. iIntros (?) "#Hinv Hγ".
    iInv N as "[$|>Hγ']" "Hclose".
    - iIntros "!==> {$Hγ} HP". iApply "Hclose"; eauto.
    - iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
  Qed.
End proofs.