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

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

8 9 10
Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.

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

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

21 22 23 24 25 26
  Global Instance :  P, AlwaysStable (saved_prop_own γ P).
  Proof.
    intros. rewrite /AlwaysStable /saved_prop_own.
    rewrite always_own; done.
  Qed.

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

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

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