From 5e7d8f0b002c47ef03b004926c3b4c17e8e5ffcc Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Mon, 29 Jun 2020 14:06:03 +0200
Subject: [PATCH] Do not require bi to be affine unnecessarily

---
 theories/bi/big_op.v              | 35 +++++++++++++++----------------
 theories/proofmode/ltac_tactics.v | 12 +++++------
 2 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index f00d5aecc..fdf1fe182 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -79,8 +79,8 @@ Section sep_list.
 
   Lemma big_sepL_nil Φ : ([∗ list] k↦y ∈ nil, Φ k y) ⊣⊢ emp.
   Proof. done. Qed.
-  Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
-  Proof. apply (affine _). Qed.
+  Lemma big_sepL_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
+  Proof. apply: affine. Qed.
   Lemma big_sepL_cons Φ x l :
     ([∗ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∗ [∗ list] k↦y ∈ l, Φ (S k) y.
   Proof. by rewrite big_opL_cons. Qed.
@@ -205,12 +205,11 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
-  Lemma big_sepL_dupl `{BiAffine PROP} P l :
+  Lemma big_sepL_dup P `{!Affine P} l :
     □ (P -∗ P ∗ P) -∗ P -∗ [∗ list] k↦x ∈ l, P.
   Proof.
-    apply wand_intro_l. induction l as [|x l IH].
-    { apply big_sepL_nil'. }
-    rewrite !big_sepL_cons //.
+    apply wand_intro_l.
+    induction l as [|x l IH]=> /=; first by apply: affine.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
     rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
   Qed.
@@ -324,8 +323,8 @@ Section sep_list2.
 
   Lemma big_sepL2_nil Φ : ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2) ⊣⊢ emp.
   Proof. done. Qed.
-  Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
-  Proof. apply (affine _). Qed.
+  Lemma big_sepL2_nil' P `{!Affine P} Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
+  Proof. apply: affine. Qed.
   Lemma big_sepL2_nil_inv_l Φ l2 :
     ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) -∗ ⌜l2 = []⌝.
   Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
@@ -852,7 +851,7 @@ Section map.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ emp.
   Proof. by rewrite big_opM_empty. Qed.
-  Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
+  Lemma big_sepM_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦x ∈ ∅, Φ k x.
   Proof. rewrite big_sepM_empty. apply: affine. Qed.
 
   Lemma big_sepM_insert Φ m i x :
@@ -1006,11 +1005,11 @@ Section map.
       by rewrite pure_True // True_impl.
   Qed.
 
-  Lemma big_sepM_dupl `{BiAffine PROP} P m :
+  Lemma big_sepM_dup P `{!Affine P} m :
     □ (P -∗ P ∗ P) -∗ P -∗ [∗ map] k↦x ∈ m, P.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
-    { apply big_sepM_empty'. }
+    { apply: big_sepM_empty'. }
     rewrite !big_sepM_insert //.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
     rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
@@ -1142,8 +1141,8 @@ Section map2.
     rewrite big_sepM2_eq /big_sepM2_def big_opM_eq pure_True ?left_id //.
     intros k. rewrite !lookup_empty; split; by inversion 1.
   Qed.
-  Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
-  Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
+  Lemma big_sepM2_empty' P `{!Affine P} Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
+  Proof. rewrite big_sepM2_empty. apply: affine. Qed.
 
   Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
   Proof.
@@ -1474,7 +1473,7 @@ Section gset.
 
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opS_empty. Qed.
-  Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
+  Lemma big_sepS_empty' P `{!Affine P} Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
   Proof. rewrite big_sepS_empty. apply: affine. Qed.
 
   Lemma big_sepS_insert Φ X x :
@@ -1594,11 +1593,11 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
-  Lemma big_sepS_dupl `{BiAffine PROP} P X :
-    □(P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
+  Lemma big_sepS_dup P `{!Affine P} X :
+    □ (P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
-    { apply big_sepS_empty'. }
+    { apply: big_sepS_empty'. }
     rewrite !big_sepS_insert //.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
     rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
@@ -1676,7 +1675,7 @@ Section gmultiset.
 
   Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opMS_empty. Qed.
-  Lemma big_sepMS_empty' `{!BiAffine PROP} P Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
+  Lemma big_sepMS_empty' P `{!Affine P} Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
   Proof. rewrite big_sepMS_empty. apply: affine. Qed.
 
   Lemma big_sepMS_disj_union Φ X Y :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2b22211f4..8709d8e26 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3246,17 +3246,17 @@ below; see the discussion in !75 for further details. *)
 Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply internal_eq_refl : core.
 Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepL_nil' : core.
+  rewrite envs_entails_eq; apply: big_sepL_nil' : core.
 Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepL2_nil' : core.
+  rewrite envs_entails_eq; apply: big_sepL2_nil' : core.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepM_empty' : core.
+  rewrite envs_entails_eq; apply: big_sepM_empty' : core.
 Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepM2_empty' : core.
+  rewrite envs_entails_eq; apply: big_sepM2_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepS_empty' : core.
+  rewrite envs_entails_eq; apply: big_sepS_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
-  rewrite envs_entails_eq; apply big_sepMS_empty' : core.
+  rewrite envs_entails_eq; apply: big_sepMS_empty' : core.
 
 (* These introduce as much as possible at once, for better performance. *)
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
-- 
GitLab