From 7fd2a3081a3971d2a7cb30e3ed46d04898d19932 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Jun 2022 15:36:15 +0200
Subject: [PATCH] Use big op properly instead of `env_map`. Simplify some
 proofs.

---
 iris/bi/lib/atomic.v          |   3 +-
 iris/proofmode/coq_tactics.v  |   4 +-
 iris/proofmode/environments.v | 111 +++++++++-------------------------
 iris/proofmode/modalities.v   |  32 +++++-----
 4 files changed, 46 insertions(+), 104 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 5750a4609..cb6927a75 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -464,7 +464,8 @@ Section proof_mode.
   Proof.
     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 bi.persistent_and_sep_assoc. apply: aupd_intro.
+    by rewrite -bi.persistent_and_sep_assoc.
   Qed.
 End proof_mode.
 
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 68f6ffafc..103bd0f6d 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -922,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)) →
-    <affine> ([∧] env_map_pers Γin) ⊢ M (<affine> ([∧] env_map_pers Γout));
+    <affine> env_and_pers Γin ⊢ M (<affine> env_and_pers Γout);
   transform_intuitionistic_env_wf : env_wf Γin → env_wf Γout;
   transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
@@ -1147,7 +1147,7 @@ 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.
-  rewrite ![([∧] _ ∧ _)%I]persistent_and_affinely_sep_l.
+  rewrite ![(env_and_pers _ ∧ _)%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.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index cce61fffb..1f605c7a4 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -78,12 +78,6 @@ Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_snoc Γ1 Γ2 i x y :
      env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
 
-Fixpoint env_map {A B} (f : A → B) (Γ : env A) : env B :=
-  match Γ with
-  | Enil => Enil
-  | Esnoc Γ j x => Esnoc (env_map f Γ) j (f x)
-  end.
-
 Inductive env_subenv {A} : relation (env A) :=
   | env_subenv_nil : env_subenv Enil Enil
   | env_subenv_snoc Γ1 Γ2 i x :
@@ -199,10 +193,6 @@ Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
 Global Instance env_to_list_proper (P : relation A) :
   Proper (env_Forall2 P ==> Forall2 P) env_to_list.
 Proof. induction 1; constructor; auto. Qed.
-Global Instance env_map_proper {B} (P : relation A) (Q : relation B) (f : A → B) :
-  Proper (P ==> Q) f →
-  Proper (env_Forall2 P ==> env_Forall2 Q) (env_map f).
-Proof. intros Hf. induction 1; constructor; auto. Qed.
 
 Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
   env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
@@ -218,40 +208,6 @@ Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
 Global Instance env_to_list_subenv_proper :
   Proper (env_subenv ==> sublist) (@env_to_list A).
 Proof. induction 1; simpl; constructor; auto. Qed.
-
-Lemma env_map_lookup {B} (f : A → B) Γ i :
-  env_map f Γ !! i = f <$> Γ !! i.
-Proof.
-  induction Γ; simpl; first done.
-  case_match; naive_solver.
-Qed.
-Lemma env_map_delete {B} (f : A → B) Γ i :
-  env_map f (env_delete i Γ) = env_delete i (env_map f Γ).
-Proof.
-  induction Γ as [|? IH]; simpl; first done.
-  case_match; first naive_solver.
-  simpl. rewrite IH. done.
-Qed.
-Lemma env_map_app {B} (f : A → B) Γ1 Γ2 :
-  env_app (env_map f Γ1) (env_map f Γ2) = (env_map f) <$> env_app Γ1 Γ2.
-Proof.
-  induction Γ1 as [|Γ1 IH i]; simpl; first done.
-  rewrite IH. clear IH.
-  destruct (env_app Γ1 Γ2) as [Γ'|]; simpl; last done.
-  rewrite env_map_lookup.
-  destruct (Γ' !! i) as [x|]; done.
-Qed.
-Lemma env_map_replace {B} (f : A → B) i Γi Γ :
-  env_replace i (env_map f Γi) (env_map f Γ) = (env_map f) <$> env_replace i Γi Γ.
-Proof.
-  induction Γ as [|Γ IH j]; simpl; first done.
-  case_match.
-  { rewrite env_map_app //. }
-  rewrite IH. clear IH.
-  rewrite env_map_lookup.
-  destruct (Γi !! _) as [x|]; simpl; first done.
-  destruct (env_replace i Γi Γ) as [Γ'|]; done.
-Qed.
 End env.
 
 Record envs (PROP : bi) := Envs {
@@ -265,14 +221,6 @@ Global Arguments env_intuitionistic {_} _.
 Global Arguments env_spatial {_} _.
 Global Arguments env_counter {_} _.
 
-Notation env_map_pers Γ := (env_map bi_persistently Γ).
-Global Instance env_persistently_persistent {PROP : bi} (Γ : env PROP) :
-  Persistent ([∧] env_map_pers Γ).
-Proof. induction Γ; simpl; apply _. Qed.
-Global Instance env_persistently_absorbing {PROP : bi} (Γ : env PROP) :
-  Absorbing ([∧] env_map_pers Γ).
-Proof. induction Γ; simpl; apply _. Qed.
-
 (** We now define the judgment [envs_entails Δ Q] for proof mode entailments.
 This judgment expresses that [Q] can be proved under the proof mode environment
 [Δ]. To improve performance and to encapsulate the internals of the proof mode
@@ -300,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_pers Γ := ([∧ list] P ∈ env_to_list Γ, <pers> P)%I.
+
 Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
-  (⌜envs_wf' Γp Γs⌝ ∧ [∧] (env_map_pers Γp) ∧ [∗] Γs)%I.
+  (⌜envs_wf' Γp Γs⌝ ∧ env_and_pers Γp ∧ [∗] Γs)%I.
 Global Instance: Params (@of_envs') 1 := {}.
 Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
   of_envs' (env_intuitionistic Δ) (env_spatial Δ).
@@ -438,16 +388,17 @@ Implicit Types P Q : PROP.
 Lemma of_envs_eq Δ :
   of_envs Δ =
   (⌜envs_wf Δ⌝ ∧
-    [∧] (env_map_pers (env_intuitionistic Δ)) ∧
+    env_and_pers (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_map_pers (env_intuitionistic Δ))) ∗ [∗] env_spatial Δ.
+  ⌜envs_wf Δ⌝ ∧ <affine> env_and_pers (env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
 Proof.
-  rewrite of_envs_eq [([∧] _ ∧ _)%I]persistent_and_affinely_sep_l persistent_and_sep_assoc //.
+  rewrite of_envs_eq [(env_and_pers _ ∧ _)%I]persistent_and_affinely_sep_l.
+  rewrite persistent_and_sep_assoc //.
 Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
@@ -492,7 +443,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).
@@ -546,20 +498,15 @@ Proof.
       naive_solver eauto using env_delete_wf, env_delete_fresh).
     rewrite -persistently_and_intuitionistically_sep_l assoc.
     apply and_mono; last done. apply and_intro.
-    + rewrite (env_lookup_perm (env_map_pers Γp)).
-      2:{ rewrite env_map_lookup. erewrite Heqo. done. }
-      simpl. rewrite and_elim_l. done.
+    + rewrite (env_lookup_perm Γp) //= and_elim_l //.
     + destruct rp; last done.
-      rewrite (env_lookup_perm (env_map_pers Γp)).
-      2:{ rewrite env_map_lookup. erewrite Heqo. done. }
-      simpl. rewrite and_elim_r. rewrite env_map_delete //.
+      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) //=.
     rewrite ![(P ∗ _)%I]comm.
-    rewrite persistent_and_sep_assoc.
-    done.
+    rewrite persistent_and_sep_assoc. done.
 Qed.
 Lemma envs_lookup_sound Δ i p P :
   envs_lookup i Δ = Some (p,P) →
@@ -576,11 +523,7 @@ Proof.
   rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
   - rewrite -persistently_and_intuitionistically_sep_l.
-    rewrite (env_lookup_perm (env_map_pers Γp)).
-    2:{ rewrite env_map_lookup. erewrite Heqo. done. }
-    rewrite !assoc. apply and_mono; last done. simpl.
-    rewrite -!assoc. apply and_mono; first done.
-    rewrite and_elim_r. rewrite env_map_delete. done.
+    rewrite (env_lookup_perm Γp) //= [(⌜_⌝ ∧ _)%I]and_elim_r !assoc //.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=.
     rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
@@ -657,7 +600,7 @@ Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
   envs_app p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ (if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
+  of_envs Δ ⊢ (if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -668,8 +611,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + apply and_intro.
-      * rewrite and_elim_l. rewrite (env_app_perm _ _ (env_map_pers Γp')).
-        2:{ erewrite env_map_app. erewrite Heqo. done. }
+      * 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,
@@ -689,7 +631,8 @@ 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 <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢
+  (if p then <affine> env_and_pers Γ 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/=.
@@ -699,12 +642,11 @@ Proof.
     + 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 _ _ (env_map_pers Γp')).
-      2:{ erewrite env_map_replace. erewrite Heqo. done. }
+    + rewrite (env_replace_perm _ _ Γp') //.
       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 env_map_delete. done.
-      * rewrite and_elim_r sep_elim_r. 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|].
@@ -724,12 +666,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 <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if p then <affine> env_and_pers Γ 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 <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
+  of_envs Δ ⊢
+  □?p P ∗ (((if p then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ') ∧
+           (□?p P -∗ of_envs Δ)).
 Proof.
   intros. apply pure_elim with (envs_wf Δ).
   { rewrite of_envs_eq. apply and_elim_l. }
@@ -748,7 +692,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 <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢
+  (if q then <affine> env_and_pers Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -762,7 +707,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 <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if q then <affine> env_and_pers Γ 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 :
@@ -864,7 +809,7 @@ Proof.
 Qed.
 
 Lemma env_to_prop_and_pers_sound Γ i P :
-  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> [∧] (env_map_pers (Esnoc Γ i P)).
+  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> env_and_pers (Esnoc Γ i P).
 Proof.
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index 315be368b..e6b7ba2cf 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -159,29 +159,25 @@ Section modality1.
     modality_spatial_action M = MIEnvId → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
-  Lemma modality_intuitionistic_forall_big_and C Γ :
+  Lemma modality_intuitionistic_forall_big_and C Ps :
     modality_intuitionistic_action M = MIEnvForall C →
-    Forall C (env_to_list Γ) →
-    <affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
+    Forall C Ps →
+    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
   Proof.
-    induction Γ as [|Γ IH i P]; intros ? HΓ; simpl.
-    - rewrite affinely_True_emp. apply modality_emp.
-    - inversion HΓ; subst. clear HΓ.
-      rewrite affinely_and -modality_and_forall //. apply and_mono.
-      + by eapply modality_intuitionistic_forall.
-      + eauto.
+    induction 2 as [|P Ps ? _ IH]; simpl.
+    { 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 Γ :
+  Lemma modality_intuitionistic_id_big_and Ps :
     modality_intuitionistic_action M = MIEnvId →
-    <affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
+    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
   Proof.
-    intros. induction Γ as [|Γ IH i P]; simpl.
-    - rewrite affinely_True_emp. apply modality_emp.
-    - rewrite affinely_and {1}IH. clear IH.
-      rewrite persistent_and_affinely_sep_l_1.
-      rewrite {1}[(<affine> <pers> P)%I]modality_intuitionistic_id //.
-      rewrite affinely_elim modality_sep. f_equiv.
-      apply: sep_and.
+    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 →
-- 
GitLab