Commit 4dacd90f authored by Ralf Jung's avatar Ralf Jung

establish that saved propositions are AlwaysStable

parent 6d147668
......@@ -70,6 +70,8 @@ Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Lemma always_own_unit γ a : ( own γ (unit a))%I own γ (unit a).
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Lemma always_own γ a : unit a a ( own γ a)%I own γ a.
Proof. by intros <-; rewrite always_own_unit. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite /own ownG_valid /to_globalF.
......@@ -83,6 +85,8 @@ 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_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
Proof. by rewrite /AlwaysStable always_own_unit. 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. *)
......
......@@ -57,6 +57,8 @@ Proof.
apply uPred.always_ownM.
by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
Qed.
Lemma always_ownG m : unit m m ( ownG m)%I ownG m.
Proof. by intros <-; rewrite always_ownG_unit. Qed.
Lemma ownG_valid m : ownG m m.
Proof.
rewrite /ownG uPred.ownM_valid res_validI /= option_validI; auto with I.
......@@ -65,6 +67,8 @@ Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
Proof. by rewrite /AlwaysStable always_ownG_unit. Qed.
(* inversion lemmas *)
Lemma ownI_spec r n i P :
......
......@@ -15,6 +15,12 @@ Section saved_prop.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types γ : gname.
Global Instance : P, AlwaysStable (saved_prop_own γ P).
Proof.
intros. rewrite /AlwaysStable /saved_prop_own.
rewrite always_own; done.
Qed.
Lemma saved_prop_alloc_strong N P (G : gset gname) :
True pvs N N ( γ, (γ G) saved_prop_own γ P).
Proof. by apply own_alloc_strong. Qed.
......
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