saved_prop.v 3.54 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.base_logic Require Export own.
2
From iris.algebra Require Import agree.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp Require Import gmap.
4
From iris.proofmode Require Import tactics.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7
Import uPred.

8 9 10 11 12 13
(* "Saved anything" -- this can give you saved propositions, saved predicates,
   saved whatever-you-like. *)

Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
14
  #[ GFunctor (agreeRF F) ].
15

16 17
Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
  subG (savedAnythingΣ F) Σ  savedAnythingG Σ F.
18
Proof. solve_inG. Qed.
19

20
Definition saved_anything_own `{savedAnythingG Σ F}
21
    (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
22
  own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
23 24
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
25

26 27
Section saved_anything.
  Context `{savedAnythingG Σ F}.
28
  Implicit Types x y : F (iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
  Implicit Types γ : gname.

31 32
  Global Instance saved_prop_persistent γ x : Persistent (saved_anything_own γ x).
  Proof. rewrite /saved_anything_own; apply _. Qed.
33

34 35
  Lemma saved_anything_alloc_strong x (G : gset gname) :
    (|==>  γ, ⌜γ  G  saved_anything_own γ x)%I.
36
  Proof. by apply own_alloc_strong. Qed.
37

38
  Lemma saved_anything_alloc x : (|==>  γ, saved_anything_own γ x)%I.
39
  Proof. by apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41 42
  Lemma saved_anything_agree γ x y :
    saved_anything_own γ x - saved_anything_own γ y - x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Proof.
44
    (* TODO: Use the proof mode. *)
45
    apply wand_intro_r.
46
    rewrite -own_op own_valid agree_validI agree_equivI.
47
    set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
48
    set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
49 50
    assert ( z, G2 (G1 z)  z) as help.
    { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
51
      apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
52
    rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  Qed.
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
End saved_anything.

(** Provide specialized versions of this for convenience. **)

(* Saved propositions. *)
Notation savedPropG Σ := (savedAnythingG Σ ( )).
Notation savedPropΣ := (savedAnythingΣ ( )).

Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
  saved_anything_own (F :=  ) γ (Next P).

Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
  (|==>  γ, saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc. Qed.

Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
  saved_prop_own γ P - saved_prop_own γ Q -  (P  Q).
Proof.
  iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
Qed.

(* Saved predicates. *)
Notation savedPredG Σ A := (savedAnythingG Σ (constCF A -n>  )).
Notation savedPredΣ A := (savedAnythingΣ (constCF A -n>  )).

Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (f: A -n> iProp Σ) :=
  saved_anything_own (F := A -n>  ) γ (CofeMor Next  f).

Lemma saved_pred_alloc `{savedPredG Σ A} (f: A -n> iProp Σ) :
  (|==>  γ, saved_pred_own γ f)%I.
Proof. iApply saved_anything_alloc. Qed.

Lemma saved_pred_agree `{savedPredG Σ A} γ f g :
  saved_pred_own γ f - saved_pred_own γ g -  x,  (f x  g x).
Proof.
  iIntros "Hx Hy *". unfold saved_pred_own. iApply later_equivI.
  iDestruct (ofe_morC_equivI (CofeMor Next  f) (CofeMor Next  g)) as "[FE _]".
  simpl. iApply ("FE" with "[-]").
  iApply (saved_anything_agree with "Hx Hy").
Qed.