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

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

Section defs.
10
  Context `{invG Σ, cinvG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16 17

  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.

18
Instance: Params (@cinv) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21
Typeclasses Opaque cinv_own cinv.

Section proofs.
22
  Context `{invG Σ, cinvG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26

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

27
  Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30 31 32 33 34
  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.

35 36 37 38
  Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
  Proof. intros ??. by rewrite -own_op. Qed.
  Global Instance cinv_own_as_fractionnal γ q :
    AsFractional (cinv_own γ q) (cinv_own γ) q.
39
  Proof. split. done. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41 42
  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
43

44 45 46 47 48
  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
49

50
  Lemma cinv_alloc E N P :  P ={E}=  γ, cinv N γ P  cinv_own γ 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
  Proof.
    rewrite /cinv /cinv_own. iIntros "HP".
53 54
    iMod (own_alloc 1%Qp) as (γ) "H1"; first done.
    iMod (inv_alloc N _ (P  own γ 1%Qp)%I with "[HP]"); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
  Qed.

57
  Lemma cinv_cancel E N γ P : N  E  cinv N γ P - cinv_own γ 1 ={E}=  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60
  Proof.
    rewrite /cinv. iIntros (?) "#Hinv Hγ".
    iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
61
    iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63 64
  Qed.

  Lemma cinv_open E N γ p P :
65
    N  E 
66
    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
67 68
  Proof.
    rewrite /cinv. iIntros (?) "#Hinv Hγ".
69
    iInv N as "[$ | >Hγ']" "Hclose".
70
    - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
71
    - iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73
  Qed.
End proofs.