Commit a3766213 authored by Robbert Krebbers's avatar Robbert Krebbers

Also rename `iPreProp` into `iPrePropO`.

parent 601625fb
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _. Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests. Section tests.
Context `{!invG Σ}. Context `{!invG Σ}.
......
...@@ -8,7 +8,7 @@ Import uPred. ...@@ -8,7 +8,7 @@ Import uPred.
Class boxG Σ := Class boxG Σ :=
boxG_inG :> inG Σ (prodR boxG_inG :> inG Σ (prodR
(authR (optionUR (exclR boolO))) (authR (optionUR (exclR boolO)))
(optionR (agreeR (laterO (iPreProp Σ))))). (optionR (agreeR (laterO (iPrePropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) * Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
optionRF (agreeRF ( )) ) ]. optionRF (agreeRF ( )) ) ].
......
...@@ -116,21 +116,21 @@ Qed. ...@@ -116,21 +116,21 @@ Qed.
the construction, this way we are sure we do not use any properties of the the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *) construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig. Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors ofeT. Parameter iPrePropO : gFunctors ofeT.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ). Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
Definition iResUR (Σ : gFunctors) : ucmraT := Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)). discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPred (iResUR Σ)). Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)). Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)). Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)). Notation iPropSI Σ := (uPredSI (iResUR Σ)).
Parameter iProp_unfold: {Σ}, iPropO Σ -n> iPreProp Σ. Parameter iProp_unfold: {Σ}, iPropO Σ -n> iPrePropO Σ.
Parameter iProp_fold: {Σ}, iPreProp Σ -n> iPropO Σ. Parameter iProp_fold: {Σ}, iPrePropO Σ -n> iPropO Σ.
Parameter iProp_fold_unfold: {Σ} (P : iProp Σ), Parameter iProp_fold_unfold: {Σ} (P : iProp Σ),
iProp_fold (iProp_unfold P) P. iProp_fold (iProp_unfold P) P.
Parameter iProp_unfold_fold: {Σ} (P : iPreProp Σ), Parameter iProp_unfold_fold: {Σ} (P : iPrePropO Σ),
iProp_unfold (iProp_fold P) P. iProp_unfold (iProp_fold P) P.
End iProp_solution_sig. End iProp_solution_sig.
...@@ -138,20 +138,20 @@ Module Export iProp_solution : iProp_solution_sig. ...@@ -138,20 +138,20 @@ Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver. Import cofe_solver.
Definition iProp_result (Σ : gFunctors) : Definition iProp_result (Σ : gFunctors) :
solution (uPredOF (iResF Σ)) := solver.result _. solution (uPredOF (iResF Σ)) := solver.result _.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ. Definition iPrePropO (Σ : gFunctors) : ofeT := iProp_result Σ.
Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _. Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT := Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)). discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPred (iResUR Σ)). Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)). Notation iPropO Σ := (uPredO (iResUR Σ)).
Definition iProp_unfold {Σ} : iPropO Σ -n> iPreProp Σ := Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
solution_fold (iProp_result Σ). solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPreProp Σ -n> iPropO Σ := solution_unfold _. Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ := solution_unfold _.
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P. Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P.
Proof. apply solution_unfold_fold. Qed. Proof. apply solution_unfold_fold. Qed.
Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) P. Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) P.
Proof. apply solution_fold_unfold. Qed. Proof. apply solution_fold_unfold. Qed.
End iProp_solution. End iProp_solution.
......
...@@ -9,10 +9,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is ...@@ -9,10 +9,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *) higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) := Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) _ }. InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPrePropO Σ) _ }.
Arguments inG_id {_ _} _. Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPreProp Σ) _). Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPrePropO Σ) _).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed. Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *) (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
......
...@@ -9,7 +9,7 @@ Import uPred. ...@@ -9,7 +9,7 @@ Import uPred.
saved whatever-you-like. *) saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG { Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _)); saved_anything_inG :> inG Σ (agreeR (F (iPrePropO Σ) _));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *) saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}. }.
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors := Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
......
...@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in ...@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *) [fancy_updates], which [wsat] is only imported. *)
Module invG. Module invG.
Class invG (Σ : gFunctors) : Set := WsatG { Class invG (Σ : gFunctors) : Set := WsatG {
inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ))))); inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inG :> inG Σ coPset_disjR; enabled_inG :> inG Σ coPset_disjR;
disabled_inG :> inG Σ (gset_disjR positive); disabled_inG :> inG Σ (gset_disjR positive);
invariant_name : gname; invariant_name : gname;
...@@ -23,7 +23,7 @@ Module invG. ...@@ -23,7 +23,7 @@ Module invG.
GFunctor (gset_disjUR positive)]. GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG { Class invPreG (Σ : gFunctors) : Set := WsatPreG {
inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ))))); inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inPreG :> inG Σ coPset_disjR; enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive); disabled_inPreG :> inG Σ (gset_disjR positive);
}. }.
...@@ -33,7 +33,7 @@ Module invG. ...@@ -33,7 +33,7 @@ Module invG.
End invG. End invG.
Import invG. Import invG.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) := Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPrePropO Σ)) :=
to_agree (Next (iProp_unfold P)). to_agree (Next (iProp_unfold P)).
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ := Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name ( {[ i := invariant_unfold P ]}). own invariant_name ( {[ i := invariant_unfold P ]}).
......
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