saved_prop.v 1.82 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
6
Notation savedPropG Λ Σ :=
  (inG Λ Σ (agreeRA (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_def `{savedPropG Λ Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
12
    (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
13
  own γ (to_agree (Next (iProp_unfold P))).
14
(* Perform sealing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
Definition saved_prop_own_aux : { x | x = @saved_prop_own_def }. by eexists. Qed.
Definition saved_prop_own {Λ Σ s} := proj1_sig saved_prop_own_aux Λ Σ s.
Definition saved_prop_own_eq :
  @saved_prop_own = @saved_prop_own_def := proj2_sig saved_prop_own_aux.

20
Instance: Params (@saved_prop_own) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
Section saved_prop.
23
  Context `{savedPropG Λ Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
  Implicit Types P Q : iPropG Λ Σ.
  Implicit Types γ : gname.

27
28
  Global Instance saved_prop_always_stable γ P :
    AlwaysStable (saved_prop_own γ P).
Ralf Jung's avatar
Ralf Jung committed
29
  Proof. by rewrite /AlwaysStable saved_prop_own_eq always_own. Qed.
30

31
  Lemma saved_prop_alloc_strong N P (G : gset gname) :
32
    True  pvs N N ( γ,  (γ  G)  saved_prop_own γ P).
Ralf Jung's avatar
Ralf Jung committed
33
  Proof. by rewrite saved_prop_own_eq; apply own_alloc_strong. Qed.
34

Robbert Krebbers's avatar
Robbert Krebbers committed
35
  Lemma saved_prop_alloc N P :
36
    True  pvs N N ( γ, saved_prop_own γ P).
Ralf Jung's avatar
Ralf Jung committed
37
  Proof. by rewrite saved_prop_own_eq; apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

39
  Lemma saved_prop_agree γ P Q :
40
    (saved_prop_own γ P  saved_prop_own γ Q)   (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  Proof.
Ralf Jung's avatar
Ralf Jung committed
42
    rewrite saved_prop_own_eq -own_op own_valid agree_validI.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
    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 Λ _,
46
      iProp_fold (iProp_unfold P)  iProp_fold Q')%I); solve_ne || auto with I.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  Qed.
48
End saved_prop.