Merge branch 'ralf/proofmode-of-envs' into 'master'

adjust proofmode of_envs to rely less on persistently_emp_2

See merge request iris/iris!794

CHANGELOG.md

@@ -44,6 +44,10 @@ lemma.
   `Forall2` (for example, for trees with finite branching).
 * Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
   implication.
+* 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,9 +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.
-    apply aupd_intro; [apply _..|]. done.
+    rewrite assoc. apply: aupd_intro. by rewrite -assoc.
   Qed.
 End proof_mode.
 

iris/proofmode/coq_tactics.v

@@ -17,7 +17,7 @@ Implicit Types P Q : PROP.
 Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
 Proof.
   rewrite envs_entails_unseal !of_envs_eq /=.
-  rewrite intuitionistically_True_emp left_id=><-.
+  rewrite left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -29,10 +29,13 @@ Lemma tac_stop Δ P :
    end ⊢ P) →
   envs_entails Δ P.
 Proof.
-  rewrite envs_entails_unseal !of_envs_eq. intros <-.
-  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
-  destruct (env_intuitionistic Δ), (env_spatial Δ);
-    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
+  rewrite envs_entails_unseal !of_envs_eq. intros <-. rewrite and_elim_r.
+  destruct (env_intuitionistic Δ).
+  { rewrite env_to_prop_sound and_elim_r //. }
+  cbv zeta. destruct (env_spatial Δ).
+  - rewrite env_to_prop_and_pers_sound. rewrite comm. done.
+  - rewrite env_to_prop_and_pers_sound env_to_prop_sound.
+    rewrite /bi_affinely [(emp ∧ _)%I]comm -persistent_and_sep_assoc left_id //.
 Qed.
 
 (** * Basic rules *)
@@ -652,7 +655,8 @@ Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
   rewrite envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
-  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
+  - rewrite (into_and _ P) /= right_id (comm _ P1).
+    rewrite -persistently_and wand_elim_r //.
   - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
 
@@ -812,7 +816,7 @@ Lemma tac_accu Δ P :
   envs_entails Δ P.
 Proof.
   rewrite envs_entails_unseal=><-.
-  rewrite env_to_prop_sound !of_envs_eq and_elim_r sep_elim_r //.
+  rewrite env_to_prop_sound !of_envs_eq and_elim_r and_elim_r //.
 Qed.
 
 (** * Invariants *)
@@ -918,7 +922,7 @@ Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
   transform_intuitionistic_env :
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
-    □ ([∧] Γin) ⊢ M (□ ([∧] Γout));
+    <affine> env_and_persistently Γin ⊢ M (<affine> env_and_persistently Γout);
   transform_intuitionistic_env_wf : env_wf Γin → env_wf Γout;
   transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
@@ -1015,7 +1019,7 @@ Section tac_modal_intro.
   Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
   Proof.
     split; [|eauto using Enil_wf|done]=> /= ??.
-    rewrite !intuitionistically_True_emp -modality_emp //.
+    rewrite !affinely_True_emp -modality_emp //.
   Qed.
   Global Instance transform_intuitionistic_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q :
     C P Q →
@@ -1023,8 +1027,11 @@ Section tac_modal_intro.
     TransformIntuitionisticEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
   Proof.
     intros ? [HΓ Hwf Hdom]; split; simpl.
-    - intros HC Hand. rewrite intuitionistically_and HC // HΓ //.
-      by rewrite Hand -intuitionistically_and.
+    - intros HC Hand. rewrite -Hand. apply and_intro.
+      + rewrite -modality_emp affinely_elim_emp. done.
+      + rewrite affinely_and HΓ //.
+        rewrite /bi_intuitionistically in HC. rewrite HC //.
+        rewrite !affinely_elim. eauto.
     - inversion 1; constructor; auto.
     - intros j. destruct (ident_beq _ _); naive_solver.
   Qed.
@@ -1090,34 +1097,32 @@ Section tac_modal_intro.
         assert (∀ i, Γs !! i = None → Γs' !! i = None).
         { destruct HΓs as [| |?????? []| |]; eauto. }
         naive_solver. }
-    assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
-    { remember (modality_intuitionistic_action M).
+    trans (<absorb>?fi Q')%I; last first.
+    { destruct fi; last done. apply: absorbing. }
+    simpl. rewrite -(HQ' Hφ). rewrite -HQ pure_True // left_id. clear HQ' HQ.
+    rewrite !persistent_and_affinely_sep_l.
+    rewrite -modality_sep absorbingly_if_sep. f_equiv.
+    - rewrite -absorbingly_if_intro.
+      remember (modality_intuitionistic_action M).
       destruct HΓp as [? M|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
-      - rewrite {1}intuitionistically_elim_emp (modality_emp M)
-          intuitionistically_True_emp //.
-      - eauto using modality_intuitionistic_forall_big_and.
-      - eauto using modality_intuitionistic_transform,
+      + rewrite !affinely_True_emp. apply modality_emp.
+      + eauto using modality_intuitionistic_forall_big_and.
+      + eauto using modality_intuitionistic_transform,
           modality_and_transform.
-      - by rewrite {1}intuitionistically_elim_emp (modality_emp M)
-          intuitionistically_True_emp.
-      - eauto using modality_intuitionistic_id. }
-    move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
-    remember (modality_spatial_action M).
-    destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
-    - by rewrite -HQ' //= !right_id.
-    - rewrite -HQ' // {1}(modality_spatial_forall_big_sep _ _ Γs) //.
-      by rewrite modality_sep.
-    - destruct fi.
-      + rewrite -(absorbing Q') /bi_absorbingly -HQ' // (comm _ True%I).
-        rewrite -modality_sep -assoc. apply sep_mono_r.
-        eauto using modality_spatial_transform.
-      + rewrite -HQ' // -modality_sep. apply sep_mono_r.
-        rewrite -(right_id emp%I bi_sep (M _)).
-        eauto using modality_spatial_transform.
-    - rewrite -HQ' //= right_id comm -{2}(modality_spatial_clear M) //.
-      by rewrite (True_intro ([∗] Γs)).
-    - rewrite -HQ' // {1}(modality_spatial_id M ([∗] Γs)) //.
-      by rewrite -modality_sep.
+      + by rewrite {1}affinely_elim_emp affinely_True_emp (modality_emp M).
+      + eauto using modality_intuitionistic_id_big_and.
+    - remember (modality_spatial_action M).
+      destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
+      + by rewrite modality_emp.
+      + rewrite {1}(modality_spatial_forall_big_sep _ _ Γs) //.
+      + destruct fi.
+        * rewrite /= /bi_absorbingly (comm _ True%I).
+          eauto using modality_spatial_transform.
+        * rewrite /= -(right_id emp%I bi_sep (M _)).
+          eauto using modality_spatial_transform.
+      + rewrite -{1}(modality_spatial_clear M) // -modality_emp.
+        rewrite absorbingly_emp_True. apply True_intro.
+      + rewrite {1}(modality_spatial_id M ([∗] Γs)) //.
   Qed.
 End tac_modal_intro.
 
@@ -1141,7 +1146,9 @@ Proof. by split. Qed.
 Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
   MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
-  intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq /= !laterN_and !laterN_sep.
+  intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq.
+  rewrite ![(env_and_persistently _ ∧ _)%I]persistent_and_affinely_sep_l.
+  rewrite !laterN_and !laterN_sep.
   rewrite -{1}laterN_intro. apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor; naive_solver.
   - apply Hp; rewrite /= /MaybeIntoLaterN.

iris/proofmode/environments.v

@@ -248,8 +248,10 @@ Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
 Definition envs_wf {PROP : bi} (Δ : envs PROP) :=
   envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
 
+Notation env_and_persistently Γ := ([∧ list] P ∈ env_to_list Γ, <pers> P)%I.
+
 Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
-  (⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs)%I.
+  (⌜envs_wf' Γp Γs⌝ ∧ env_and_persistently Γp ∧ [∗] Γs)%I.
 Global Instance: Params (@of_envs') 1 := {}.
 Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
   of_envs' (env_intuitionistic Δ) (env_spatial Δ).
@@ -384,13 +386,24 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ =
+  (⌜envs_wf Δ⌝ ∧
+    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 Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
-Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.
+
+Lemma of_envs'_alt Γp Γs :
+  of_envs' Γp Γs ⊣⊢ ⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs.
+Proof.
+  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).
@@ -434,7 +447,8 @@ Proof.
   intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply and_mono; simpl in *.
   - apply pure_mono=> -[???]. constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - by repeat f_equiv.
+  - f_equiv; [|by repeat f_equiv].
+    induction Hp; simpl; repeat (done || f_equiv).
 Qed.
 Global Instance of_envs_proper' :
   Proper (env_Forall2 (⊣⊢) ==> env_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs' PROP).
@@ -483,18 +497,20 @@ Lemma envs_lookup_sound' Δ rp i p P :
 Proof.
   rewrite /envs_lookup /envs_delete !of_envs_eq=>?.
   apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
   - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    destruct rp.
-    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
-      by rewrite and_sep_intuitionistically -assoc.
-    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
-      by rewrite intuitionistically_and and_elim_l -assoc.
+    rewrite -persistently_and_intuitionistically_sep_l assoc.
+    apply and_mono; last done. apply and_intro.
+    + rewrite (env_lookup_perm Γp) //= and_elim_l //.
+    + destruct rp; last done.
+      rewrite (env_lookup_perm Γp) //= and_elim_r //.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
+    rewrite (env_lookup_perm Γs) //=.
+    rewrite ![(P ∗ _)%I]comm.
+    rewrite persistent_and_sep_assoc. done.
 Qed.
 Lemma envs_lookup_sound Δ i p P :
   envs_lookup i Δ = Some (p,P) →
@@ -509,11 +525,14 @@ Lemma envs_lookup_sound_2 Δ i p P :
 Proof.
   rewrite /envs_lookup !of_envs_eq=>Hwf ?.
   rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - by rewrite (env_lookup_perm Γp) //= intuitionistically_and
-      and_sep_intuitionistically and_elim_r assoc.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
+  - rewrite -persistently_and_intuitionistically_sep_l.
+    rewrite (env_lookup_perm Γp) //= [(⌜_⌝ ∧ _)%I]and_elim_r !assoc //.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
-    by rewrite (env_lookup_perm Γs) //= and_elim_r !assoc (comm _ P).
+    rewrite (env_lookup_perm Γs) //=.
+    rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
+    rewrite (comm _ P) -persistent_and_sep_assoc.
+    apply and_mono; first done. rewrite comm //.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
@@ -575,35 +594,39 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
+    + rewrite -persistently_and_intuitionistically_sep_l assoc //.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + by rewrite !assoc (comm _ P).
+    + rewrite (comm _ P) -persistent_and_sep_assoc.
+      apply and_mono; first done. rewrite comm //.
 Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
   envs_app p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs Δ ⊢ (if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
   - destruct (env_app Γ Γs) eqn:Happ,
-      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+      (env_app Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
-    + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
-      by rewrite assoc.
+    + apply and_intro.
+      * rewrite and_elim_l. rewrite (env_app_perm _ _ Γp') //.
+        rewrite affinely_elim big_opL_app sep_and. done.
+      * rewrite and_elim_r. rewrite sep_elim_r. done.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
-    + by rewrite (env_app_perm _ _ Γs') // big_opL_app !assoc (comm _ ([∗] Γ)%I).
+    + rewrite (env_app_perm _ _ Γs') // big_opL_app. apply and_intro.
+      * rewrite and_elim_l. rewrite sep_elim_r. done.
+      * rewrite and_elim_r. done.
 Qed.
 
 Lemma envs_app_singleton_sound Δ Δ' p j Q :
@@ -612,19 +635,22 @@ Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢
+  (if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
   - destruct (env_app Γ Γs) eqn:Happ,
-      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+      (env_replace i Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
-      by rewrite assoc.
+      rewrite big_opL_app. apply and_intro; first apply and_intro.
+      * rewrite and_elim_l affinely_elim sep_elim_l. done.
+      * rewrite sep_elim_r and_elim_l //.
+      * rewrite and_elim_r sep_elim_r //.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -632,7 +658,9 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γs') // big_opL_app.
-      by rewrite !assoc (comm _ ([∗] Γ)%I).
+      apply and_intro.
+      * rewrite and_elim_l. rewrite sep_elim_r. done.
+      * rewrite and_elim_r. done.
 Qed.
 
 Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
@@ -642,12 +670,14 @@ Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Q
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
+  of_envs Δ ⊢
+  □?p P ∗ (((if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ') ∧
+           (□?p P -∗ of_envs Δ)).
 Proof.
   intros. apply pure_elim with (envs_wf Δ).
   { rewrite of_envs_eq. apply and_elim_l. }
@@ -666,7 +696,8 @@ Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢
+  (if q then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -680,7 +711,7 @@ Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if q then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
@@ -702,16 +733,18 @@ Lemma envs_clear_spatial_sound Δ :
   of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
 Proof.
   rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
-  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
-  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
+  rewrite -persistent_and_sep_assoc. apply and_intro.
+  - apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
+  - rewrite -persistent_and_sep_assoc left_id. done.
 Qed.
 
 Lemma env_spatial_is_nil_intuitionistically Δ :
   env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
 Proof.
   intros. rewrite !of_envs_eq; destruct Δ as [? []]; simplify_eq/=.
-  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
-  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
+  rewrite /bi_intuitionistically !persistently_and.
+  rewrite persistently_pure persistent_persistently -persistently_emp_2.
+  apply and_intro; last done. rewrite !and_elim_r. done.
 Qed.
 
 Lemma envs_lookup_envs_delete Δ i p P :
@@ -779,11 +812,13 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma env_to_prop_and_sound Γ : env_to_prop_and Γ ⊣⊢ [∧] Γ.
+Lemma env_to_prop_and_pers_sound Γ i P :
+  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> env_and_persistently (Esnoc Γ i P).
 Proof.
-  destruct Γ as [|Γ i P]; simpl; first done.
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
-  - rewrite /= IH (comm _ Q _) assoc. done.
+  - rewrite /= IH. clear IH. f_equiv. simpl.
+    rewrite assoc. f_equiv.
+    rewrite persistently_and comm. done.
 Qed.
 End envs.

iris/proofmode/modalities.v

@@ -160,12 +160,23 @@ Section modality1.
 
   Lemma modality_intuitionistic_forall_big_and C Ps :
     modality_intuitionistic_action M = MIEnvForall C →
-    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
+    Forall C Ps →
+    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
   Proof.
     induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite intuitionistically_True_emp -modality_emp.
-    - rewrite intuitionistically_and -modality_and_forall // -IH.
-      by rewrite {1}(modality_intuitionistic_forall _ P).
+    { rewrite affinely_True_emp. apply modality_emp. }
+    rewrite affinely_and -modality_and_forall //. apply and_mono, IH.
+    by eapply modality_intuitionistic_forall.
+  Qed.
+  Lemma modality_intuitionistic_id_big_and Ps :
+    modality_intuitionistic_action M = MIEnvId →
+    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
+  Proof.
+    intros. induction Ps as [|P Ps IH]; simpl.
+    { rewrite affinely_True_emp. apply modality_emp. }
+    rewrite -affinely_and_r. rewrite {1}IH {IH}.
+    rewrite !persistently_and_intuitionistically_sep_l.
+    by rewrite {1}(modality_intuitionistic_id P) // modality_sep.
   Qed.
   Lemma modality_spatial_forall_big_sep C Ps :
     modality_spatial_action M = MIEnvForall C →

iris/proofmode/reduction.v

@@ -4,7 +4,9 @@ From iris.prelude Require Import options.
 
 (** Called by all tactics to perform computation to lookup items in the
     context.  We avoid reducing anything user-visible here to make sure we
-    do not reduce e.g. before unification happens in [iApply].*)
+    do not reduce e.g. before unification happens in [iApply].
+    This needs to contain all definitions used in the user-visible statements in
+    [coq_tactics], and their dependencies. *)
 Declare Reduction pm_eval := cbv [
   (* base *)
   base.negb base.beq