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

5
Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
6 7
  saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))).
Definition savedPropGF (F : cFunctor) : gFunctor :=
8
  GFunctor (agreeRF ( F)).
9 10
Instance inGF_savedPropG  `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
Proof. apply: inGF_inG. Qed.
11

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

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

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

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

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

34
  Lemma saved_prop_agree γ x y :
35
    (saved_prop_own γ x  saved_prop_own γ y)  (x  y).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  Proof.
37
    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
38 39 40
    set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
    set (G2 := cFunctor_map F (@iProp_unfold Λ (globalF Σ),
                               @iProp_fold Λ (globalF Σ))).
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.