Commit b962b90e authored by Robbert Krebbers's avatar Robbert Krebbers

Type class for persistent CMRA elements.

parent 9459fc48
Pipeline #343 passed with stage
......@@ -118,6 +118,9 @@ Proof.
Qed.
Canonical Structure agreeR : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
Global Instance agree_persistent (x : agree A) : Persistent x.
Proof. done. Qed.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
......
......@@ -120,6 +120,10 @@ Class CMRAUnit (A : cmraT) `{Empty A} := {
}.
Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate .
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : core x x.
Arguments persistent {_} _ {_}.
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) := {
cmra_discrete :> Discrete A;
......@@ -229,6 +233,8 @@ Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_core_valid x : x core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
Global Instance cmra_core_persistent x : Persistent (core x).
Proof. apply cmra_core_idemp. Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x y x {n} y.
......@@ -336,8 +342,8 @@ Section unit.
Proof. by exists x; rewrite left_id. Qed.
Global Instance cmra_unit_right_id : RightId () ().
Proof. by intros x; rewrite (comm op) left_id. Qed.
Lemma cmra_core_unit : core .
Proof. by rewrite -{2}(cmra_core_l ) right_id. Qed.
Global Instance cmra_unit_persistent : Persistent .
Proof. by rewrite /Persistent -{2}(cmra_core_l ) right_id. Qed.
End unit.
(** ** Local updates *)
......@@ -454,6 +460,8 @@ Section cmra_transport.
Proof. by destruct H. Qed.
Global Instance cmra_transport_timeless x : Timeless x Timeless (T x).
Proof. by destruct H. Qed.
Global Instance cmra_transport_persistent x : Persistent x Persistent (T x).
Proof. by destruct H. Qed.
Lemma cmra_transport_updateP (P : A Prop) (Q : B Prop) x :
x ~~>: P ( y, P y Q (T y)) T x ~~>: Q.
Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
......@@ -509,6 +517,8 @@ Section unit.
Global Instance unit_cmra_unit : CMRAUnit unitR.
Global Instance unit_cmra_discrete : CMRADiscrete unitR.
Proof. by apply discrete_cmra_discrete. Qed.
Global Instance unit_persistent (x : ()) : Persistent x.
Proof. done. Qed.
End unit.
(** ** Product *)
......@@ -564,6 +574,10 @@ Section prod.
CMRADiscrete A CMRADiscrete B CMRADiscrete prodR.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
Global Instance pair_persistent x y :
Persistent x Persistent y Persistent (x,y).
Proof. by split. Qed.
Lemma prod_update x y : x.1 ~~> y.1 x.2 ~~> y.2 x ~~> y.
Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
Lemma prod_updateP P1 P2 (Q : A * B Prop) x :
......
......@@ -45,7 +45,7 @@ Qed.
Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
(* Some properties of this CMRA *)
Lemma dec_agree_core_id (x : dec_agree A) : core x = x.
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. done. Qed.
Lemma dec_agree_ne a b : a b DecAgree a DecAgree b = DecAgreeBot.
......
......@@ -215,6 +215,12 @@ Lemma map_op_singleton (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance map_persistent m : ( x : A, Persistent x) Persistent m.
Proof. intros ? i. by rewrite lookup_core persistent. Qed.
Global Instance map_singleton_persistent i (x : A) :
Persistent x Persistent {[ i := x ]}.
Proof. intros. by rewrite /Persistent map_core_singleton persistent. Qed.
Lemma singleton_includedN n m i x :
{[ i := x ]} {n} m y, m !! i {n} Some y x {n} y.
Proof.
......
......@@ -208,11 +208,15 @@ Section iprod_cmra.
Lemma iprod_core_singleton x (y : B x) :
core (iprod_singleton x y) iprod_singleton x (core y).
Proof.
by move=>x'; destruct (decide (x = x')) as [->|];
rewrite iprod_lookup_core ?iprod_lookup_singleton
?iprod_lookup_singleton_ne // cmra_core_unit.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite iprod_lookup_core ?iprod_lookup_singleton
?iprod_lookup_singleton_ne // (persistent ).
Qed.
Global Instance iprod_singleton_persistent x (y : B x) :
Persistent y Persistent (iprod_singleton x y).
Proof. intros. rewrite /Persistent iprod_core_singleton. by f_equiv. Qed.
Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
iprod_singleton x y1 iprod_singleton x y2 iprod_singleton x (y1 y2).
Proof.
......
......@@ -210,16 +210,15 @@ Proof.
intros [|a| |]; simpl; auto using cmra_discrete_valid.
Qed.
Global Instance Shot_persistent a : Persistent a Persistent (Shot a).
Proof. by constructor. Qed.
Lemma one_shot_validN_inv_l n y : {n} (OneShotPending y) y = .
Proof.
destruct y as [|b| |]; [done| |done|done]. destruct 1.
Qed.
Proof. by destruct y; inversion_clear 1. Qed.
Lemma one_shot_valid_inv_l y : (OneShotPending y) y = .
Proof. intros. by apply one_shot_validN_inv_l with 0, cmra_valid_validN. Qed.
Lemma one_shot_bot_largest y : y OneShotBot.
Proof.
destruct y; exists OneShotBot; constructor.
Qed.
Proof. destruct y; exists OneShotBot; constructor. Qed.
(** Internalized properties *)
Lemma one_shot_equivI {M} (x y : one_shot A) :
......@@ -259,9 +258,8 @@ Proof.
- destruct (Hx n b) as (c&?&?); try done.
exists (Shot c). auto.
- destruct (Hx n (core a)) as (c&?&?); try done.
{ rewrite cmra_core_r. done. }
exists (Shot c). split; first by auto.
simpl. by eapply cmra_validN_op_l.
{ by rewrite cmra_core_r. }
exists (Shot c). split; simpl; eauto using cmra_validN_op_l.
Qed.
Lemma one_shot_updateP' (P : A Prop) a :
a ~~>: P Shot a ~~>: λ m', b, m' = Shot b P b.
......
......@@ -130,6 +130,12 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
Lemma option_op_positive_dist_r n mx my : mx my {n} None my {n} None.
Proof. by destruct mx, my; inversion_clear 1. Qed.
Global Instance Some_persistent (x : A) : Persistent x Persistent (Some x).
Proof. by constructor. Qed.
Global Instance option_persistent (mx : option A) :
( x : A, Persistent x) Persistent mx.
Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
(x y) ⊣⊢ (match x, y with
......
......@@ -304,8 +304,8 @@ Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}.
Class Persistent {M} (P : uPred M) := persistent : P P.
Arguments persistent {_} _ {_}.
Class PersistentP {M} (P : uPred M) := persistentP : P P.
Arguments persistentP {_} _ {_}.
Module uPred.
Definition unseal :=
......@@ -1002,8 +1002,8 @@ Proof.
rewrite -(cmra_core_idemp a) Hx.
apply cmra_core_preservingN, cmra_includedN_l.
Qed.
Lemma always_ownM (a : M) : core a a ( uPred_ownM a) ⊣⊢ uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_core. Qed.
Lemma always_ownM (a : M) : Persistent a ( uPred_ownM a) ⊣⊢ uPred_ownM a.
Proof. intros. by rewrite -(persistent a) always_ownM_core. Qed.
Lemma ownM_something : True a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
Lemma ownM_empty `{Empty M, !CMRAUnit M} : True uPred_ownM .
......@@ -1120,53 +1120,53 @@ Proof.
Qed.
(* Always stable *)
Global Instance const_persistent φ : Persistent ( φ : uPred M)%I.
Proof. by rewrite /Persistent always_const. Qed.
Global Instance always_persistent P : Persistent ( P).
Global Instance const_persistent φ : PersistentP ( φ : uPred M)%I.
Proof. by rewrite /PersistentP always_const. Qed.
Global Instance always_persistent P : PersistentP ( P).
Proof. by intros; apply always_intro'. Qed.
Global Instance and_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_and; apply and_mono. Qed.
PersistentP P PersistentP Q PersistentP (P Q).
Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
Global Instance or_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_or; apply or_mono. Qed.
PersistentP P PersistentP Q PersistentP (P Q).
Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
Global Instance sep_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. by intros; rewrite /Persistent always_sep; apply sep_mono. Qed.
PersistentP P PersistentP Q PersistentP (P Q).
Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
Global Instance forall_persistent {A} (Ψ : A uPred M) :
( x, Persistent (Ψ x)) Persistent ( x, Ψ x).
Proof. by intros; rewrite /Persistent always_forall; apply forall_mono. Qed.
( x, PersistentP (Ψ x)) PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
Global Instance exist_persistent {A} (Ψ : A uPred M) :
( x, Persistent (Ψ x)) Persistent ( x, Ψ x).
Proof. by intros; rewrite /Persistent always_exist; apply exist_mono. Qed.
( x, PersistentP (Ψ x)) PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
Global Instance eq_persistent {A : cofeT} (a b : A) :
Persistent (a b : uPred M)%I.
Proof. by intros; rewrite /Persistent always_eq. Qed.
PersistentP (a b : uPred M)%I.
Proof. by intros; rewrite /PersistentP always_eq. Qed.
Global Instance valid_persistent {A : cmraT} (a : A) :
Persistent ( a : uPred M)%I.
Proof. by intros; rewrite /Persistent always_valid. Qed.
Global Instance later_persistent P : Persistent P Persistent ( P).
Proof. by intros; rewrite /Persistent always_later; apply later_mono. Qed.
Global Instance ownM_core_persistent (a : M) : Persistent (uPred_ownM (core a)).
Proof. by rewrite /Persistent always_ownM_core. Qed.
PersistentP ( a : uPred M)%I.
Proof. by intros; rewrite /PersistentP always_valid. Qed.
Global Instance later_persistent P : PersistentP P PersistentP ( P).
Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
Global Instance ownM_persistent : Persistent a PersistentP (@uPred_ownM M a).
Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global Instance default_persistent {A} P (Ψ : A uPred M) (mx : option A) :
Persistent P ( x, Persistent (Ψ x)) Persistent (default P mx Ψ).
PersistentP P ( x, PersistentP (Ψ x)) PersistentP (default P mx Ψ).
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for always stable *)
Lemma always_always P `{!Persistent P} : ( P) ⊣⊢ P.
Lemma always_always P `{!PersistentP P} : ( P) ⊣⊢ P.
Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_intro P Q `{!Persistent P} : P Q P Q.
Lemma always_intro P Q `{!PersistentP P} : P Q P Q.
Proof. rewrite -(always_always P); apply always_intro'. Qed.
Lemma always_and_sep_l P Q `{!Persistent P} : (P Q) ⊣⊢ (P Q).
Lemma always_and_sep_l P Q `{!PersistentP P} : (P Q) ⊣⊢ (P Q).
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
Lemma always_and_sep_r P Q `{!Persistent Q} : (P Q) ⊣⊢ (P Q).
Lemma always_and_sep_r P Q `{!PersistentP Q} : (P Q) ⊣⊢ (P Q).
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
Lemma always_sep_dup P `{!Persistent P} : P ⊣⊢ (P P).
Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ (P P).
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
Lemma always_entails_l P Q `{!Persistent Q} : (P Q) P (Q P).
Lemma always_entails_l P Q `{!PersistentP Q} : (P Q) P (Q P).
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r P Q `{!Persistent Q} : (P Q) P (P Q).
Lemma always_entails_r P Q `{!PersistentP Q} : (P Q) P (P Q).
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End uPred_logic.
......
......@@ -30,7 +30,7 @@ Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
(** * Always stability for lists *)
Class PersistentL {M} (Ps : list (uPred M)) :=
persistentL : Forall Persistent Ps.
persistentL : Forall PersistentP Ps.
Arguments persistentL {_} _ {_}.
Section big_op.
......@@ -216,21 +216,21 @@ Section gset.
End gset.
(* Always stable *)
Global Instance big_and_persistent Ps : PersistentL Ps Persistent (Π∧ Ps).
Global Instance big_and_persistent Ps : PersistentL Ps PersistentP (Π∧ Ps).
Proof. induction 1; apply _. Qed.
Global Instance big_sep_persistent Ps : PersistentL Ps Persistent (Π★ Ps).
Global Instance big_sep_persistent Ps : PersistentL Ps PersistentP (Π★ Ps).
Proof. induction 1; apply _. Qed.
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_persistent P Ps :
Persistent P PersistentL Ps PersistentL (P :: Ps).
PersistentP P PersistentL Ps PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_persistent Ps Ps' :
PersistentL Ps PersistentL Ps' PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance zip_with_persistent {A B} (f : A B uPred M) xs ys :
( x y, Persistent (f x y)) PersistentL (zip_with f xs ys).
( x y, PersistentP (f x y)) PersistentL (zip_with f xs ys).
Proof.
unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
......
......@@ -51,7 +51,7 @@ Definition recv (l : loc) (R : iProp) : iProp :=
saved_prop_own i Q (Q - R))%I.
Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
Persistent (barrier_ctx γ l P).
PersistentP (barrier_ctx γ l P).
Proof. apply _. Qed.
(* TODO: Figure out if this has a "Global" or "Local" effect.
......
......@@ -33,7 +33,7 @@ Section definitions.
Global Instance heap_inv_proper : Proper (() ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_persistent N : Persistent (heap_ctx N).
Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
......
......@@ -103,9 +103,7 @@ Proof.
rewrite -(exist_intro n). ecancel [inv _ _]%I.
rewrite [(_ _)%I]comm -assoc. apply const_elim_sep_l=>->.
rewrite const_equiv // left_id /one_shot_inv -or_intro_r.
rewrite -(exist_intro n).
rewrite -(dec_agree_core_id (DecAgree n))
-(Shot_core (DecAgree n : dec_agreeR _)) {1}(always_sep_dup (own _ _)).
rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
solve_sep_entails. }
cancel [one_shot_inv γ l].
(* FIXME: why aren't laters stripped? *)
......
......@@ -30,7 +30,7 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless a : TimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_ctx_persistent N φ : Persistent (auth_ctx N φ).
Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
Proof. apply _. Qed.
End definitions.
......
......@@ -36,10 +36,6 @@ Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ (own γ a1 ★ own γ a2).
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Lemma always_own_core γ a : ( own γ (core a)) ⊣⊢ own γ (core a).
Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
Lemma always_own γ a : core a a ( own γ a) ⊣⊢ own γ a.
Proof. by intros <-; rewrite always_own_core. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite /own ownG_valid /to_globalF.
......@@ -53,9 +49,9 @@ Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ( a own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own γ a).
Proof. unfold own; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent (own γ (core a)).
Proof. by rewrite /Persistent always_own_core. Qed.
Proof. rewrite /own; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a PersistentP (own γ a).
Proof. rewrite /own; apply _. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
......
......@@ -41,12 +41,10 @@ Lemma to_globalF_op γ a1 a2 :
Proof.
by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
Qed.
Lemma to_globalF_core γ a : core (to_globalF γ a) to_globalF γ (core a).
Proof.
by rewrite /to_globalF
iprod_core_singleton map_core_singleton cmra_transport_core.
Qed.
Global Instance to_globalF_timeless γ m : Timeless m Timeless (to_globalF γ m).
Global Instance to_globalF_timeless γ m: Timeless m Timeless (to_globalF γ m).
Proof. rewrite /to_globalF; apply _. Qed.
Global Instance to_globalF_persistent γ m :
Persistent m Persistent (to_globalF γ m).
Proof. rewrite /to_globalF; apply _. Qed.
End to_globalF.
......
......@@ -23,7 +23,7 @@ Implicit Types Φ : val Λ → iProp Λ Σ.
Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
Global Instance inv_persistent N P : Persistent (inv N P).
Global Instance inv_persistent N P : PersistentP (inv N P).
Proof. rewrite /inv; apply _. Qed.
Lemma always_inv N P : ( inv N P) ⊣⊢ inv N P.
......@@ -96,5 +96,4 @@ Proof.
intros. rewrite -(pvs_mask_weaken N) //.
by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
Qed.
End inv.
......@@ -25,15 +25,8 @@ Proof.
apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
by apply Next_contractive=> j ?; rewrite (HPQ j).
Qed.
Lemma always_ownI i P : ( ownI i P) ⊣⊢ ownI i P.
Proof.
apply uPred.always_ownM.
by rewrite Res_core !cmra_core_unit map_core_singleton.
Qed.
Global Instance ownI_persistent i P : Persistent (ownI i P).
Proof. by rewrite /Persistent always_ownI. Qed.
Lemma ownI_sep_dup i P : ownI i P ⊣⊢ (ownI i P ownI i P).
Proof. apply (uPred.always_sep_dup _). Qed.
Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
(* physical state *)
Lemma ownP_twice σ1 σ2 : (ownP σ1 ownP σ2 : iProp Λ Σ) False.
......@@ -52,25 +45,16 @@ Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ (ownG m1 ★ ownG m2).
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
Lemma always_ownG_core m : ( ownG (core m)) ⊣⊢ ownG (core m).
Proof.
apply uPred.always_ownM.
by rewrite Res_core !cmra_core_unit -{2}(cmra_core_idemp m).
Qed.
Lemma always_ownG m : core m m ( ownG m) ⊣⊢ ownG m.
Proof. by intros <-; rewrite always_ownG_core. Qed.
Lemma ownG_valid m : ownG m m.
Proof.
rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
Qed.
Proof. rewrite /ownG uPred.ownM_valid res_validI /=; auto with I. Qed.
Lemma ownG_valid_r m : ownG m (ownG m m).
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Lemma ownG_empty : True (ownG : iProp Λ Σ).
Proof. apply uPred.ownM_empty. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_core_persistent m : Persistent (ownG (core m)).
Proof. by rewrite /Persistent always_ownG_core. Qed.
Global Instance ownG_persistent m : Persistent m PersistentP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *)
Lemma ownI_spec n r i P :
......
......@@ -146,10 +146,10 @@ Lemma pvs_strip_pvs E P Q : P ⊢ (|={E}=> Q) → (|={E}=> P) ⊢ (|={E}=> Q).
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P |={E1,E2}=> Q) (|={E1,E2}=> P Q).
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!Persistent P} :
Lemma pvs_always_l E1 E2 P Q `{!PersistentP P} :
(P |={E1,E2}=> Q) (|={E1,E2}=> P Q).
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!Persistent Q} :
Lemma pvs_always_r E1 E2 P Q `{!PersistentP Q} :
((|={E1,E2}=> P) Q) (|={E1,E2}=> P Q).
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
Lemma pvs_impl_l E1 E2 P Q : ( (P Q) (|={E1,E2}=> P)) (|={E1,E2}=> Q).
......
......@@ -153,6 +153,8 @@ Lemma lookup_wld_op_r n r1 r2 i P :
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Global Instance Res_timeless eσ m : Timeless m Timeless (@Res Λ A M eσ m).
Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
Global Instance Res_persistent w m: Persistent m Persistent (@Res Λ A M w m).
Proof. constructor; apply (persistent _). Qed.
(** Internalized properties *)
Lemma res_equivI {M'} r1 r2 :
......
......@@ -9,8 +9,7 @@ Definition oneShotGF (F : cFunctor) : gFunctor :=
Instance inGF_oneShotG `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
Proof. apply: inGF_inG. Qed.
Definition one_shot_pending `{oneShotG Λ Σ F}
(γ : gname) : iPropG Λ Σ :=
Definition one_shot_pending `{oneShotG Λ Σ F} (γ : gname) : iPropG Λ Σ :=
own γ OneShotPending.
Definition one_shot_own `{oneShotG Λ Σ F}
(γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ :=
......@@ -23,9 +22,8 @@ Section one_shot.
Implicit Types x y : F (iPropG Λ Σ).
Implicit Types γ : gname.
Global Instance ne_shot_own_persistent γ x :
Persistent (one_shot_own γ x).
Proof. by rewrite /Persistent always_own. Qed.
Global Instance ne_shot_own_persistent γ x : PersistentP (one_shot_own γ x).
Proof. rewrite /one_shot_own; apply _. Qed.
Lemma one_shot_alloc_strong N (G : gset gname) :
True pvs N N ( γ, (γ G) one_shot_pending γ).
......
......@@ -20,9 +20,8 @@ Section saved_prop.
Implicit Types x y : F (iPropG Λ Σ).
Implicit Types γ : gname.
Global Instance saved_prop_persistent γ x :
Persistent (saved_prop_own γ x).
Proof. by rewrite /Persistent always_own. Qed.
Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
Proof. rewrite /saved_prop_own; apply _. Qed.
Lemma saved_prop_alloc_strong N x (G : gset gname) :
True pvs N N ( γ, (γ G) saved_prop_own γ x).
......
......@@ -42,7 +42,7 @@ Section definitions.
Global Instance sts_ctx_proper N :
Proper (pointwise_relation _ () ==> (⊣⊢)) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_persistent N φ : Persistent (sts_ctx N φ).
Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sts_own sts_ownS sts_ctx.
......
......@@ -239,10 +239,10 @@ Proof.
rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
apply wp_frame_step_r.
Qed.
Lemma wp_always_l E e Φ R `{!Persistent R} :
Lemma wp_always_l E e Φ R `{!PersistentP R} :
(R WP e @ E {{ Φ }}) WP e @ E {{ λ v, R Φ v }}.
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
Lemma wp_always_r E e Φ R `{!Persistent R} :
Lemma wp_always_r E e Φ R `{!PersistentP R} :
(WP e @ E {{ Φ }} R) WP e @ E {{ λ v, Φ v R }}.
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma wp_impl_l E e Φ Ψ :
......
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