saved_prop.v 1.49 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From algebra Require Export agree.
2
From program_logic Require Export global_functor.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4
Import uPred.

5
Notation savedPropG Λ Σ :=
6
  (inG Λ Σ (agreeR (laterC (iPreProp Λ (globalF Σ))))).
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
9
Proof. apply: inGF_inG. Qed.
10

11
Definition saved_prop_own `{savedPropG Λ Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
12
    (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
13
  own γ (to_agree (Next (iProp_unfold P))).
14
Typeclasses Opaque saved_prop_own.
15
Instance: Params (@saved_prop_own) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

17
Section saved_prop.
18
  Context `{savedPropG Λ Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21
  Implicit Types P Q : iPropG Λ Σ.
  Implicit Types γ : gname.

22 23
  Global Instance saved_prop_always_stable γ P :
    AlwaysStable (saved_prop_own γ P).
24
  Proof. by rewrite /AlwaysStable always_own. Qed.
25

26
  Lemma saved_prop_alloc_strong N P (G : gset gname) :
27
    True  pvs N N ( γ,  (γ  G)  saved_prop_own γ P).
28
  Proof. by apply own_alloc_strong. Qed.
29

Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Lemma saved_prop_alloc N P :
31
    True  pvs N N ( γ, saved_prop_own γ P).
32
  Proof. by apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

34
  Lemma saved_prop_agree γ P Q :
35
    (saved_prop_own γ P  saved_prop_own γ Q)   (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  Proof.
37
    rewrite -own_op own_valid agree_validI.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40
    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 Λ _,
41
      iProp_fold (iProp_unfold P)  iProp_fold Q')%I); solve_proper || auto with I.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  Qed.
43
End saved_prop.