saved_prop.v 5.12 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Import gmap.
2
From iris.algebra Require Import agree.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.proofmode Require Import proofmode.
4
From iris.base_logic Require Export own.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.prelude Require Import options.
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 (oFunctor_apply F (iPropO Σ)));
13
  saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
14
}.
15
Local Existing Instance saved_anything_inG.
16

17
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
18
  #[ GFunctor (agreeRF F) ].
19

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

24
Definition saved_anything_own `{!savedAnythingG Σ F}
25
    (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
26
  own γ (to_agree x).
27
Typeclasses Opaque saved_anything_own.
28
Global Instance: Params (@saved_anything_own) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

30
Section saved_anything.
31
  Context `{!savedAnythingG Σ F}.
32
  Implicit Types x y : oFunctor_apply F (iPropO Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
  Implicit Types γ : gname.

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

39
40
41
42
43
  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
44
45
  Lemma saved_anything_alloc_strong x (I : gname  Prop) :
    pred_infinite I 
46
     |==>  γ, I γ⌝  saved_anything_own γ x.
Dan Frumin's avatar
Dan Frumin committed
47
48
49
  Proof. intros ?. by apply own_alloc_strong. Qed.

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

Gregory Malecha's avatar
Gregory Malecha committed
53
  Lemma saved_anything_alloc x :  |==>  γ, saved_anything_own γ x.
54
  Proof. by apply own_alloc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55

56
57
  Lemma saved_anything_agree γ x y :
    saved_anything_own γ x - saved_anything_own γ y - x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  Proof.
59
60
    iIntros "Hx Hy". rewrite /saved_anything_own.
    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
61
    by rewrite agree_validI agree_equivI.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Qed.
63
64
65
66
67
68
69
70
End saved_anything.

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

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

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

74
Global Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
75
  Contractive (saved_prop_own γ).
Ralf Jung's avatar
Ralf Jung committed
76
Proof. solve_contractive. Qed.
77

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

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

87
Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
88
   |==>  γ, saved_prop_own γ P.
89
90
Proof. iApply saved_anything_alloc. Qed.

91
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
92
93
  saved_prop_own γ P - saved_prop_own γ Q -  (P  Q).
Proof.
94
95
  iIntros "HP HQ". iApply later_equivI.
  iApply (saved_anything_agree (F :=  ) with "HP HQ").
96
97
98
Qed.

(* Saved predicates. *)
99
100
Notation savedPredG Σ A := (savedAnythingG Σ (A -d>  )).
Notation savedPredΣ A := (savedAnythingΣ (A -d>  )).
101

102
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A  iProp Σ) :=
Ralf Jung's avatar
Ralf Jung committed
103
  saved_anything_own (F := A -d>  ) γ (Next  Φ).
104

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

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

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

120
Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A  iProp Σ) :
Gregory Malecha's avatar
Gregory Malecha committed
121
   |==>  γ, saved_pred_own γ Φ.
122
123
Proof. iApply saved_anything_alloc. Qed.

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