From 12137966d0561845ca9ec96e0bcb23586445af80 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 12:55:50 +0200
Subject: [PATCH] weaken affinity assumptions; properly seal make_laterable_id

---
 iris/bi/lib/atomic.v          | 26 ++++++++++++++++----------
 iris/bi/lib/laterable.v       | 13 ++++++-------
 iris/proofmode/ltac_tactics.v |  2 +-
 3 files changed, 23 insertions(+), 18 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 5c3c3c61f..6e7ddd53b 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -449,13 +449,18 @@ Section proof_mode.
   then apply coinduction, and then introduce the modality (the last two steps
   happen inside [aupd_intro]). We instead we define a dummy modality [make_laterable_id] that also
   uses [MIEnvTransform IntoLaterable] and use that to pre-process the goal. *)
-  Local Definition make_laterable_id (P : PROP) := P.
+  Local Definition make_laterable_id_def (P : PROP) := P.
+  Local Definition make_laterable_id_aux : seal make_laterable_id_def.
+  Proof. by eexists. Qed.
+  Local Definition make_laterable_id := make_laterable_id_aux.(unseal).
+  Local Definition make_laterable_id_eq : make_laterable_id = make_laterable_id_def :=
+    make_laterable_id_aux.(seal_eq).
 
   Local Lemma modality_make_laterable_id_mixin :
     modality_mixin make_laterable_id MIEnvId (MIEnvTransform IntoLaterable).
   Proof.
-    split; simpl; eauto.
-    - intros P Q ?. rewrite (into_laterable P). done.
+    rewrite make_laterable_id_eq. split; simpl; eauto.
+    intros P Q ?. rewrite (into_laterable P). done.
   Qed.
 
   Local Definition modality_make_laterable_id :=
@@ -467,16 +472,16 @@ Section proof_mode.
 
   Local Lemma make_laterable_id_elim P :
     make_laterable_id P -∗ P.
-  Proof. done. Qed.
+  Proof. rewrite make_laterable_id_eq. done. Qed.
 
-  (** We need [PROP] to be affine as otherwise [emp] is not [Laterable]. *)
-  Lemma tac_aupd_intro `{!BiAffine PROP} Γp Γs n α β Eo Ei Φ P :
+  Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
+    Laterable (PROP:=PROP) emp →
     TCForall Laterable (env_to_list Γs) →
     P = env_to_prop Γs →
     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_eq of_envs_eq' /atomic_acc /=.
+    intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
     setoid_rewrite env_to_prop_sound =>HAU.
     apply aupd_intro; [apply _..|]. done.
   Qed.
@@ -489,8 +494,9 @@ Local Ltac iMakeLaterable :=
   iApply make_laterable_id_elim; iModIntro.
 
 Tactic Notation "iAuIntro" :=
-  iMakeLaterable; eapply tac_aupd_intro; [
-    iSolveTC || fail "bug in iMakeLaterable: context not laterable"
+  iMakeLaterable; notypeclasses refine (tac_aupd_intro _ _ _ _ _ _ _ _ _ _ _ _ _); [
+    iSolveTC || fail "iAuIntro: emp not laterable"
+  | iSolveTC || fail "iAuIntro: context not laterable; this should not happen, please report a bug"
   | (* P = ...: make the P pretty *) pm_reflexivity
   | (* the new proof mode goal *) ].
 
@@ -506,4 +512,4 @@ Tactic Notation "iAaccIntro" "with" constr(sel) :=
   end.
 
 (* From here on, prevent TC search from implicitly unfolding these. *)
-Typeclasses Opaque atomic_acc atomic_update make_laterable_id.
+Typeclasses Opaque atomic_acc atomic_update.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 0dee7157d..bfc5093c1 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -89,7 +89,7 @@ Section instances.
   Qed.
 
   Global Instance big_sepL_laterable Ps :
-    Timeless (PROP:=PROP) emp →
+    Laterable (PROP:=PROP) emp →
     TCForall Laterable Ps →
     Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
@@ -195,7 +195,7 @@ Section instances.
     - trans (make_laterable (â—‡ Q)).
       + apply make_laterable_mono, make_laterable_elim.
       + apply make_laterable_except_0.
-    - iApply make_laterable_intro'.
+    - apply make_laterable_intro', _.
   Qed.
 
   Lemma laterable_alt Q :
@@ -220,20 +220,19 @@ Section instances.
     IntoLaterable P (â–· P) | 100.
   Proof. constructor; last by apply _. apply bi.later_intro. Qed.
 
-  (** We need PROP to be affine as otherwise [emp] is not [Laterable]. *)
-  Lemma modality_make_laterable_mixin `{!BiAffine PROP} :
+  Lemma modality_make_laterable_mixin `{!Timeless (PROP:=PROP) emp} :
     modality_mixin make_laterable MIEnvId (MIEnvTransform IntoLaterable).
   Proof.
     split; simpl; eauto using make_laterable_intro', make_laterable_mono,
-      make_laterable_sep with typeclass_instances.
+      make_laterable_sep, intuitionistic_laterable with typeclass_instances.
     - intros P Q ?. rewrite (into_laterable P).
       apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _.
   Qed.
 
-  Definition modality_make_laterable `{!BiAffine PROP} :=
+  Definition modality_make_laterable `{!Timeless (PROP:=PROP) emp} :=
     Modality _ modality_make_laterable_mixin.
 
-  Global Instance from_modal_make_laterable `{!BiAffine PROP} P :
+  Global Instance from_modal_make_laterable `{!Timeless (PROP:=PROP) emp} P :
     FromModal True modality_make_laterable (make_laterable P) (make_laterable P) P.
   Proof. by rewrite /FromModal. Qed.
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index bfd12ae7b..d9ab16e89 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2623,7 +2623,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      not have this issue. *)
   notypeclasses refine (tac_löb _ IH _ _ _ _);
     [iSolveTC || fail "iLöb: no 'BiLöb' instance found"
-    |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
+    |reflexivity || fail "iLöb: spatial context not empty; this should not happen, please report a bug"
     |pm_reduce;
      lazymatch goal with
      | |- False =>
-- 
GitLab