saved_prop.v 1.79 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.base_logic Require Export own.
2
From iris.algebra Require Import agree.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp Require Import gmap.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
Import uPred.

7
Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
8 9 10
  saved_prop_inG :> inG Σ (agreeR (F (iPreProp Σ))).
Definition savedPropΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
  #[ GFunctor (agreeRF F) ].
11

12 13
Instance subG_savedPropΣ {Σ F} `{!cFunctorContractive F} :
  subG (savedPropΣ F) Σ  savedPropG Σ F.
14
Proof. solve_inG. Qed.
15

16 17
Definition saved_prop_own `{savedPropG Σ F}
    (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
18
  own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
19
Typeclasses Opaque saved_prop_own.
20
Instance: Params (@saved_prop_own) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
Section saved_prop.
23 24
  Context `{savedPropG Σ F}.
  Implicit Types x y : F (iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26
  Implicit Types γ : gname.

27
  Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
28
  Proof. rewrite /saved_prop_own; apply _. Qed.
29

30
  Lemma saved_prop_alloc_strong x (G : gset gname) :
31
    (|==>  γ, ⌜γ  G  saved_prop_own γ x)%I.
32
  Proof. by apply own_alloc_strong. Qed.
33

34
  Lemma saved_prop_alloc x : (|==>  γ, saved_prop_own γ x)%I.
35
  Proof. by apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37
  Lemma saved_prop_agree γ x y :
38
    saved_prop_own γ x - saved_prop_own γ y - x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Proof.
40
    apply wand_intro_r.
41
    rewrite -own_op own_valid agree_validI agree_equivI.
42
    set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
43
    set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
44 45
    assert ( z, G2 (G1 z)  z) as help.
    { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
46
      apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
47
    rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  Qed.
49
End saved_prop.