Viewshifts from ∅.

program_logic/pviewshifts.v

@@ -99,11 +99,22 @@ Qed.
 Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
-  intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
-  destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P) as (m'&?&?); auto.
+  intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
   { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
+Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+    E (P : iGst Λ Σ → Prop) :
+  ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
+Proof.
+  intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
+  { apply cmra_empty_leastN. }
+  { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
+      auto using option_update_None. }
+  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
+Qed.
 Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ inv i P).
 Proof.
   intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
@@ -138,7 +149,7 @@ Proof.
 Qed.
 Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
 Proof.
-  intros; rewrite ->(pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
+  intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
 End pvs.

program_logic/viewshifts.v

@@ -89,6 +89,10 @@ Qed.
 Lemma vs_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
+Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
+    E (P : iGst Λ Σ → Prop) :
+  ∅ ~~>: P → True >{E}> (∃ m', ■ P m' ∧ ownG m').
+Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed.
 Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
 Proof. by intros; apply vs_alt, pvs_update. Qed.
 Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ inv i P).

program_logic/wsat.v

@@ -125,13 +125,13 @@ Proof.
   split; [done|exists rs].
   by constructor; split_ands'; try (rewrite /= -associative Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
-  Some m1 ≼{S n} gst r → m1 ~~>: P →
+Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
+  mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
-  intros [mf Hr] Hup%option_updateP' [rs [(?&?&?) Hσ HE Hwld]].
+  intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
   destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) n) as ([m2|]&?&Hval'); try done.
-  { by rewrite /= (associative _ (Some m1)) -Hr associative. }
+  { by rewrite /= (associative _ mm1) -Hr associative. }
   exists m2; split; [exists rs; split; split_ands'; auto|done].
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :