saved_prop.v 1.86 KB
Newer Older
1
From iris.program_logic Require Export ghost_ownership.
2 3
From iris.algebra Require Import agree.
From iris.prelude Require Import gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Import uPred.

6 7
Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
  saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
8 9
Definition savedPropΣ (F : cFunctor) : gFunctors :=
  #[ GFunctor (agreeRF ( F)) ].
10

11 12
Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ  savedPropG Σ F.
Proof. apply subG_inG. Qed.
13

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

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

25 26
  Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
  Proof. rewrite /saved_prop_own; apply _. Qed.
27

28 29
  Lemma saved_prop_alloc_strong x (G : gset gname) :
    True =r=>  γ,  (γ  G)  saved_prop_own γ x.
30
  Proof. by apply own_alloc_strong. Qed.
31

32
  Lemma saved_prop_alloc x : True =r=>  γ, saved_prop_own γ x.
33
  Proof. by apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
34

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