cancelable_invariants.v 2.45 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
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
Import uPred.

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

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

  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.

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

Section proofs.
21
  Context `{invG Σ, cinvG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
29
30
31
32
33
34

  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 :
35
    cinv_own γ q1  cinv_own γ q2  cinv_own γ (q1 + q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
  Proof. by rewrite /cinv_own own_op. Qed.

38
  Lemma cinv_own_half γ q : cinv_own γ (q/2)  cinv_own γ (q/2)  cinv_own γ q.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
  Proof. by rewrite cinv_own_op Qp_div_2. Qed.

41
  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
  Lemma cinv_own_1_l γ q : cinv_own γ 1  cinv_own γ q  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
  Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.

47
  Lemma cinv_alloc E N P :  P ={E}=  γ, cinv N γ P  cinv_own γ 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
  Proof.
    rewrite /cinv /cinv_own. iIntros "HP".
50
51
    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
52
53
54
  Qed.

  Lemma cinv_cancel E N γ P :
55
    nclose N  E  cinv N γ P  cinv_own γ 1 ={E}=  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
58
59
60
61
62
63
  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 
64
    cinv N γ P  cinv_own γ p ={E,EN}=  P  cinv_own γ p  ( P ={EN,E}= True).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
  Proof.
    rewrite /cinv. iIntros (?) "#Hinv Hγ".
    iInv N as "[$|>Hγ']" "Hclose".
68
    - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
    - iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
  Qed.
End proofs.