saved_prop.v 5.23 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
Typeclasses Opaque saved_anything_own.
24
Instance: Params (@saved_anything_own) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
25

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

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

35 36 37 38 39
  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
40 41 42 43 44 45
  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) :
46
    (|==>  γ, ⌜γ  G  saved_anything_own γ x)%I.
Dan Frumin's avatar
Dan Frumin committed
47
  Proof. by apply own_alloc_cofinite. Qed.
48

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

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

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
80 81 82 83 84 85
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 Σ) :
86
  (|==>  γ, ⌜γ  G  saved_prop_own γ P)%I.
Dan Frumin's avatar
Dan Frumin committed
87
Proof. iApply saved_anything_alloc_cofinite. Qed.
88

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

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

103
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A  iProp Σ) :=
104
  saved_anything_own (F := A -c>  ) γ (CofeMor Next  Φ).
105

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

Dan Frumin's avatar
Dan Frumin committed
112 113 114 115 116 117
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 Σ) :
118
  (|==>  γ, ⌜γ  G  saved_pred_own γ Φ)%I.
Dan Frumin's avatar
Dan Frumin committed
119
Proof. iApply saved_anything_alloc_cofinite. Qed.
120

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

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