Merge branch 'ralf/saved_prop' into 'master'

generalize savedProp to let the user control the position of the type-level later

See merge request FP/iris-coq!76

theories/algebra/ofe.v

@@ -620,9 +620,9 @@ Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
 Instance: Params (@ccompose) 3.
 Infix "◎" := ccompose (at level 40, left associativity).
-Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
-  f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2.
-Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
+Global Instance ccompose_ne {A B C} :
+  NonExpansive2 (@ccompose A B C).
+Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
 
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')

theories/base_logic/lib/saved_prop.v

 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
-  saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
-Definition savedPropΣ (F : cFunctor) : gFunctors :=
-  #[ GFunctor (agreeRF (▶ F)) ].
+(* "Saved anything" -- this can give you saved propositions, saved predicates,
+   saved whatever-you-like. *)
 
-Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
+Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
+  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+  #[ GFunctor (agreeRF F) ].
+
+Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
+  subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
-Definition saved_prop_own `{savedPropG Σ F}
+Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
-  own γ (to_agree $ Next (cFunctor_map F (iProp_fold, iProp_unfold) x)).
-Typeclasses Opaque saved_prop_own.
-Instance: Params (@saved_prop_own) 3.
+  own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
+Typeclasses Opaque saved_anything_own.
+Instance: Params (@saved_anything_own) 3.
 
-Section saved_prop.
-  Context `{savedPropG Σ F}.
+Section saved_anything.
+  Context `{savedAnythingG Σ F}.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
-  Proof. rewrite /saved_prop_own; apply _. Qed.
+  Global Instance saved_anything_persistent γ x :
+    Persistent (saved_anything_own γ x).
+  Proof. rewrite /saved_anything_own; apply _. Qed.
+
+  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.
 
-  Lemma saved_prop_alloc_strong x (G : gset gname) :
-    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc_strong x (G : gset gname) :
+    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc x : (|==> ∃ γ, saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
   Proof. by apply own_alloc. Qed.
 
-  Lemma saved_prop_agree γ x y :
-    saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
+  Lemma saved_anything_agree γ x y :
+    saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
   Proof.
-    apply wand_intro_r.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+    iIntros "Hx Hy". rewrite /saved_anything_own.
+    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
+    rewrite agree_validI agree_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
+    rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
   Qed.
-End saved_prop.
+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).
+
+Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+  Contractive (saved_prop_own γ).
+Proof. solve_contractive. Qed.
+
+Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+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) (Φ : A -n> iProp Σ) :=
+  saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ).
+
+Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ).
+Proof.
+  solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | f_contractive | f_equiv ]).
+Qed.
+
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A -n> iProp Σ) :
+  (|==> ∃ γ, saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+(* We put the `x` on the outside to make this lemma easier to apply. *)
+Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+  saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
+Proof.
+  iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
+  iDestruct (ofe_morC_equivI (CofeMor Next ◎ Φ) (CofeMor Next ◎ Ψ)) as "[FE _]".
+  simpl. iApply ("FE" with "[-]").
+  iApply (saved_anything_agree with "HΦ HΨ").
+Qed.