remove of_envs_eq'; add of_envs_alt

CHANGELOG.md

@@ -47,6 +47,7 @@ lemma.
 * Change `of_envs` such that when the persistent context is empty, the
   persistence modality no longer appears at all. This is a step towards using
   the proofmode in logics without a persistence modality.
+  The lemma `of_envs_alt` shows equivalence with the old version.
 
 **Changes in `base_logic`:**
 

iris/bi/lib/atomic.v

@@ -274,15 +274,15 @@ Section lemmas.
   Qed.
 
   Lemma aupd_intro P Q α β Eo Ei Φ :
-    Affine P → Persistent P → Laterable Q →
-    (P ∗ Q -∗ atomic_acc Eo Ei α Q β Φ) →
-    P ∗ Q -∗ atomic_update Eo Ei α β Φ.
+    Absorbing P → Persistent P → Laterable Q →
+    (P ∧ Q -∗ atomic_acc Eo Ei α Q β Φ) →
+    P ∧ Q -∗ atomic_update Eo Ei α β Φ.
   Proof.
     rewrite atomic_update_unseal {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
     iApply (greatest_fixpoint_coiter _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
     iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> HQ".
-    iApply HAU. by iFrame.
+    iApply HAU. iSplit; by iFrame.
   Qed.
 
   Lemma aacc_intro Eo Ei α P β Φ :
@@ -462,10 +462,9 @@ Section proof_mode.
     envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
     envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
   Proof.
-    intros ? HΓs ->. rewrite envs_entails_unseal of_envs_eq' /atomic_acc /=.
+    intros ? HΓs ->. rewrite envs_entails_unseal of_envs_eq /atomic_acc /=.
     setoid_rewrite env_to_prop_sound =>HAU.
-    rewrite bi.persistent_and_sep_assoc. apply: aupd_intro.
-    by rewrite -bi.persistent_and_sep_assoc.
+    rewrite assoc. apply: aupd_intro. by rewrite -assoc.
   Qed.
 End proof_mode.
 

iris/proofmode/environments.v

@@ -391,15 +391,19 @@ Lemma of_envs_eq Δ :
     env_and_persistently (env_intuitionistic Δ) ∧
     [∗] env_spatial Δ)%I.
 Proof. done. Qed.
-(** An environment is a ∗ of something intuitionistic and the spatial environment.
-TODO: Can we define it as such? *)
-Lemma of_envs_eq' Δ :
-  of_envs Δ ⊣⊢
-  ⌜envs_wf Δ⌝ ∧ <affine> env_and_persistently (env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
+
+Lemma of_envs'_alt Γp Γs :
+  of_envs' Γp Γs ⊣⊢ ⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs.
 Proof.
-  rewrite of_envs_eq [(env_and_persistently _ ∧ _)%I]persistent_and_affinely_sep_l.
-  rewrite persistent_and_sep_assoc //.
+  rewrite /of_envs'. f_equiv.
+  rewrite -persistent_and_affinely_sep_l. f_equiv.
+  clear. induction Γp as [|Γp IH ? Q]; simpl.
+  { apply (anti_symm (⊢)); last by apply True_intro. apply persistently_True. }
+  rewrite IH persistently_and. done.
 Qed.
+Lemma of_envs_alt Δ :
+  of_envs Δ ⊣⊢ ⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ.
+Proof. rewrite /of_envs of_envs'_alt //. Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).