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

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

11
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
12
  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _));
13
  saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
14
}.
15
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
16
  #[ GFunctor (agreeRF F) ].
17

18
Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
19
  subG (savedAnythingΣ F) Σ  savedAnythingG Σ F.
20
Proof. solve_inG. Qed.
21

22
Definition saved_anything_own `{!savedAnythingG Σ F}
23
    (γ : gname) (x : F (iProp Σ) _) : iProp Σ :=
24
  own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
25
Typeclasses Opaque saved_anything_own.
26
Instance: Params (@saved_anything_own) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

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

Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
  Global Instance saved_anything_persistent γ x :
    Persistent (saved_anything_own γ x).
35
  Proof. rewrite /saved_anything_own; apply _. Qed.
36

37 38 39 40 41
  Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
  Proof. solve_proper. Qed.
  Global Instance saved_anything_proper γ : Proper (() ==> ()) (saved_anything_own γ).
  Proof. solve_proper. Qed.

Dan Frumin's avatar
Dan Frumin committed
42 43 44 45 46 47
  Lemma saved_anything_alloc_strong x (I : gname  Prop) :
    pred_infinite I 
    (|==>  γ, I γ⌝  saved_anything_own γ x)%I.
  Proof. intros ?. by apply own_alloc_strong. Qed.

  Lemma saved_anything_alloc_cofinite x (G : gset gname) :
48
    (|==>  γ, ⌜γ  G  saved_anything_own γ x)%I.
Dan Frumin's avatar
Dan Frumin committed
49
  Proof. by apply own_alloc_cofinite. Qed.
50

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

54 55
  Lemma saved_anything_agree γ x y :
    saved_anything_own γ x - saved_anything_own γ y - x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Proof.
57 58 59
    iIntros "Hx Hy". rewrite /saved_anything_own.
    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
    rewrite agree_validI agree_equivI.
60 61
    set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
    set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
62
    assert ( z, G2 (G1 z)  z) as help.
63 64
    { intros z. rewrite /G1 /G2 -oFunctor_compose -{2}[z]oFunctor_id.
      apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
65
    rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  Qed.
67 68 69 70 71 72 73 74
End saved_anything.

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

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

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

78
Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
79
  Contractive (saved_prop_own γ).
Ralf Jung's avatar
Ralf Jung committed
80
Proof. solve_contractive. Qed.
81

Dan Frumin's avatar
Dan Frumin committed
82 83 84 85 86 87
Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname  Prop) (P: iProp Σ) :
  pred_infinite I 
  (|==>  γ, I γ⌝  saved_prop_own γ P)%I.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.

Lemma saved_prop_alloc_cofinite `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
88
  (|==>  γ, ⌜γ  G  saved_prop_own γ P)%I.
Dan Frumin's avatar
Dan Frumin committed
89
Proof. iApply saved_anything_alloc_cofinite. Qed.
90

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

95
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
96 97 98 99 100 101
  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. *)
102 103
Notation savedPredG Σ A := (savedAnythingG Σ (A -d>  )).
Notation savedPredΣ A := (savedAnythingΣ (A -d>  )).
104

105
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A  iProp Σ) :=
106
  saved_anything_own (F := A -d>  ) γ (OfeMor Next  Φ).
107

108
Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
109
  Contractive (saved_pred_own γ : (A -d> iProp Σ)  iProp Σ).
110
Proof.
111
  solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
112 113
Qed.

Dan Frumin's avatar
Dan Frumin committed
114 115 116 117 118 119
Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname  Prop) (Φ : A  iProp Σ) :
  pred_infinite I 
  (|==>  γ, I γ⌝  saved_pred_own γ Φ)%I.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.

Lemma saved_pred_alloc_cofinite `{!savedPredG Σ A} (G : gset gname) (Φ : A  iProp Σ) :
120
  (|==>  γ, ⌜γ  G  saved_pred_own γ Φ)%I.
Dan Frumin's avatar
Dan Frumin committed
121
Proof. iApply saved_anything_alloc_cofinite. Qed.
122

123
Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A  iProp Σ) :
124
  (|==>  γ, saved_pred_own γ Φ)%I.
125 126
Proof. iApply saved_anything_alloc. Qed.

127
(* We put the `x` on the outside to make this lemma easier to apply. *)
128
Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
129
  saved_pred_own γ Φ - saved_pred_own γ Ψ -  (Φ x  Ψ x).
130
Proof.
131 132
  unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
  iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq".
133
  by iDestruct (discrete_fun_equivI with "Heq") as "?".
134
Qed.