saved_prop.v 1.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
From algebra Require Export agree.
From program_logic Require Export ghost_ownership.
Import uPred.

Class SavedPropInG Λ Σ (i : gid) :=
  saved_prop_inG :> InG Λ Σ i (agreeRA (laterC (iPreProp Λ (globalF Σ)))).

Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i}
    (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
  own i γ (to_agree (Next (iProp_unfold P))).
Instance: Params (@saved_prop_own) 5.

13
Section saved_prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
  Context `{SavedPropInG Λ Σ SPI}.
  Implicit Types P Q : iPropG Λ Σ.
  Implicit Types γ : gname.

18
  Lemma saved_prop_alloc_strong N P (G : gset gname) :
19
    True  pvs N N ( γ,  (γ  G)  saved_prop_own SPI γ P).
20
21
  Proof. by apply own_alloc_strong. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
  Lemma saved_prop_alloc N P :
    True  pvs N N ( γ, saved_prop_own SPI γ P).
  Proof. by apply own_alloc. Qed.

26
  Lemma saved_prop_agree γ P Q :
27
    (saved_prop_own SPI γ P  saved_prop_own SPI γ Q)   (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
  Proof.
    rewrite /saved_prop_own -own_op own_valid agree_validI.
    rewrite agree_equivI later_equivI /=; apply later_mono.
    rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
    apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
33
      iProp_fold (iProp_unfold P)  iProp_fold Q')%I); solve_ne || auto with I.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  Qed.
35
End saved_prop.