Merge branch 'ralf/au-intro' into 'master'

make iAuIntro smarter

See merge request iris/iris!806

iris/bi/lib/atomic.v

@@ -456,15 +456,18 @@ Section proof_mode.
   Proof. rewrite make_laterable_id_eq. done. Qed.
 
   Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
-    Laterable (PROP:=PROP) emp →
+    match Γs with Enil => Laterable (PROP:=PROP) emp | _ => TCTrue end →
     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_unseal of_envs_eq /atomic_acc /=.
+    intros Hemp HΓs ->. rewrite envs_entails_unseal of_envs_eq /atomic_acc /=.
     setoid_rewrite env_to_prop_sound =>HAU.
-    rewrite assoc. apply: aupd_intro. by rewrite -assoc.
+    rewrite assoc. apply: aupd_intro.
+    { destruct Γs as [|Γs i P]; first done.
+      inversion HΓs. simpl. apply big_sep_sepL_laterable; done. }
+    by rewrite -assoc.
   Qed.
 End proof_mode.
 
@@ -475,18 +478,23 @@ Local Ltac iMakeLaterable :=
   iApply make_laterable_id_elim; iModIntro.
 
 Tactic Notation "iAuIntro" :=
-  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 *) ].
+  iMakeLaterable;
+  match goal with
+  | |- envs_entails (Envs ?Γp ?Γs _) (atomic_update _ _ _ _ ?Φ) =>
+      notypeclasses refine (tac_aupd_intro Γp Γs _ _ _ _ _ Φ _ _ _ _ _); [
+        (* The [match Γs] precondition *)
+        iSolveTC || fail "iAuIntro: spacial context empty, and 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 *) ]
+  end.
 
 (** Tactic to apply [aacc_intro]. This only really works well when you have
 [α ?] already and pass it as [iAaccIntro with "Hα"]. Doing
 [rewrite /atomic_acc /=] is an entirely legitimate alternative. *)
 Tactic Notation "iAaccIntro" "with" constr(sel) :=
   iStartProof; lazymatch goal with
-  | |- environments.envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
+  | |- envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
     iApply (@aacc_intro PROP H TA TB Eo Ei α P β Φ with sel);
     first try solve_ndisj; last iSplit
   | _ => fail "iAAccIntro: Goal is not an atomic accessor"

iris/bi/lib/laterable.v

@@ -88,11 +88,25 @@ Section instances.
     iExists Q. iIntros "{$HQ} !> HQ". iExists x. by iApply "HΦ".
   Qed.
 
+  Lemma big_sep_sepL_laterable Q Ps :
+    Laterable Q →
+    TCForall Laterable Ps →
+    Laterable (Q ∗ [∗] Ps).
+  Proof.
+    intros HQ HPs. revert Q HQ. induction HPs as [|P Ps ?? IH]; intros Q HQ.
+    { simpl. rewrite right_id. done. }
+    simpl. rewrite assoc. apply IH; by apply _.
+  Qed.
+
   Global Instance big_sepL_laterable Ps :
     Laterable (PROP:=PROP) emp →
     TCForall Laterable Ps →
     Laterable ([∗] Ps).
-  Proof. induction 2; simpl; apply _. Qed.
+  Proof.
+    intros. assert (Laterable (emp ∗ [∗] Ps)) as Hlater.
+    { apply big_sep_sepL_laterable; done. }
+    rewrite ->left_id in Hlater; last by apply _. done.
+  Qed.
 
   (** A wrapper to obtain a weaker, laterable form of any assertion.
      Alternatively: the modality corresponding to [Laterable].

tests/atomic.ref

+The command has indeed failed with message:
+Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
 1 goal
   
   Σ : gFunctors

tests/atomic.v

@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
-Section definition.
+Section general_bi_tests.
   Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
 
   (** We can quantify over telescopes *inside* Iris and use them with atomic
@@ -14,7 +14,17 @@ Section definition.
   Definition AU_tele_quantify_iris : Prop :=
     ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
         atomic_update Eo Ei α β Φ.
-End definition.
+
+  (** iAuIntro works with non-empty laterable spacial context without any further
+  assumptions. *)
+  Lemma au_intro_1 (P : PROP) `{!Laterable P} (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    P -∗ atomic_update Eo Ei α β Φ.
+  Proof. iIntros "HP". iAuIntro. Abort.
+  (** But in an empty context, it fails, since [emp] now needs to be laterable. *)
+  Lemma au_intro_2 (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    ⊢ atomic_update Eo Ei α β Φ.
+  Proof. Fail iAuIntro. Abort.
+End general_bi_tests.
 
 Section tests.
   Context `{!heapGS Σ} {aheap: atomic_heap Σ}.