Commit 143eb81a authored by Ralf Jung's avatar Ralf Jung

explain to be careful around savedAnythingG

parent a1cf5cb9
...@@ -683,6 +683,7 @@ Bind Scope cFunctor_scope with cFunctor. ...@@ -683,6 +683,7 @@ Bind Scope cFunctor_scope with cFunctor.
Class cFunctorContractive (F : cFunctor) := Class cFunctorContractive (F : cFunctor) :=
cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
Hint Mode cFunctorContractive ! : typeclass_instances.
Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A. Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
Coercion cFunctor_diag : cFunctor >-> Funclass. Coercion cFunctor_diag : cFunctor >-> Funclass.
......
...@@ -5,14 +5,25 @@ From iris.proofmode Require Import tactics. ...@@ -5,14 +5,25 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
(* "Saved anything" -- this can give you saved propositions, saved predicates, (**
saved whatever-you-like. *) "Saved anything" -- this can give you saved propositions, saved predicates,
saved whatever-you-like.
However, be careful when using [savedAnythingG] directly: make sure the functor
you pass is actually contractive! If you don't, you might end up accidentally
relying on a proof of `False` by assuming the existence of an impossible domain
for your ghost state. Better define an abstraction of top of this that
has a sanity check such as [subG_savedPropG] below.
*)
Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))). saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors := Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ]. #[ GFunctor (agreeRF F) ].
(* This makes an extra assumption [cFunctorContractive], meaning
you can only actually have [savedAnythingG] if your [F] is contractive!
This is why you have to be careful (see above) *)
Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} : Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
subG (savedAnythingΣ F) Σ savedAnythingG Σ F. subG (savedAnythingΣ F) Σ savedAnythingG Σ F.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
...@@ -64,6 +75,9 @@ End saved_anything. ...@@ -64,6 +75,9 @@ End saved_anything.
(* Saved propositions. *) (* Saved propositions. *)
Notation savedPropG Σ := (savedAnythingG Σ ( )). Notation savedPropG Σ := (savedAnythingG Σ ( )).
Notation savedPropΣ := (savedAnythingΣ ( )). Notation savedPropΣ := (savedAnythingΣ ( )).
(* Sanity check: [savedPropΣ] does not need any extra assumptions. *)
Lemma subG_savedPropG {Σ} : subG savedPropΣ Σ savedPropG Σ.
Proof. apply _. Qed.
Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) := Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
saved_anything_own (F := ) γ (Next P). saved_anything_own (F := ) γ (Next P).
...@@ -89,6 +103,9 @@ Qed. ...@@ -89,6 +103,9 @@ Qed.
(* Saved predicates. *) (* Saved predicates. *)
Notation savedPredG Σ A := (savedAnythingG Σ (A -c> )). Notation savedPredG Σ A := (savedAnythingG Σ (A -c> )).
Notation savedPredΣ A := (savedAnythingΣ (A -c> )). Notation savedPredΣ A := (savedAnythingΣ (A -c> )).
(* Sanity check: [savedPropΣ] does not need any extra assumptions. *)
Lemma subG_savedPredG {Σ A} : subG (savedPredΣ A) Σ savedPredG Σ A.
Proof. apply _. Qed.
Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A iProp Σ) := Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A iProp Σ) :=
saved_anything_own (F := A -c> ) γ (CofeMor Next Φ). saved_anything_own (F := A -c> ) γ (CofeMor Next Φ).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment