Let iLöb automatically revert and introduce spatial hypotheses.

algebra/upred.v

@@ -796,6 +796,12 @@ Proof.
 Qed.
 Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ (P -★ Q).
 Proof. auto using wand_intro_l. Qed.
+Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R).
+Proof.
+  apply (anti_symm _).
+  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
+  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
+Qed.
 
 Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q).
 Proof. auto. Qed.

heap_lang/lib/barrier/proof.v

@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) :
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
-  iLöb "Hγ HQR HΦ" as "IH". wp_rec. wp_focus (! _)%E.
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
   wp_load. destruct p.
   - (* a Low state. The comparison fails, and we recurse. *)

heap_lang/lib/spawn.v

@@ -75,7 +75,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
   (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join (%l) {{ Φ }}.
 Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
-  iLöb "Hγ Hv" as "IH". wp_rec. wp_focus (! _)%E.
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].

proofmode/coq_tactics.v

@@ -85,6 +85,9 @@ Definition envs_split {M}
 Definition envs_persistent {M} (Δ : envs M) :=
   if env_spatial Δ is Enil then true else false.
 
+Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
+  Envs (env_persistent Δ) Enil.
+
 (* Coq versions of the tactics *)
 Section tactics.
 Context {M : cmraT}.
@@ -92,6 +95,10 @@ Implicit Types Γ : env (uPred M).
 Implicit Types Δ : envs M.
 Implicit Types P Q : uPred M.
 
+Lemma of_envs_def Δ :
+  of_envs Δ = (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+Proof. done. Qed.
+
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
   envs_lookup_delete i Δ = Some (p,P,Δ')
   ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete i p Δ.
@@ -227,9 +234,23 @@ Proof.
       env_split_fresh_1, env_split_fresh_2.
 Qed.
 
-Lemma env_special_nil_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
+Lemma envs_clear_spatial_sound Δ :
+  Δ ⊢ (envs_clear_spatial Δ ★ Π★ env_spatial Δ)%I.
+Proof.
+  rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
+  rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
+  destruct Hwf; constructor; simpl; auto using Enil_wf.
+Qed.
+
+Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ⊣⊢ (Π★ Γ -★ Q).
+Proof.
+  revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
+  by rewrite IH wand_curry (comm uPred_sep).
+Qed.
+
+Lemma envs_persistent_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
-Hint Immediate env_special_nil_persistent : typeclass_instances.
+Hint Immediate envs_persistent_persistent : typeclass_instances.
 
 (** * Adequacy *)
 Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
@@ -253,9 +274,9 @@ Qed.
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') → Δ' ⊢ Q → Δ ⊢ Q.
 Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
-Lemma tac_clear_spatial Δ Δ1 Δ2 Q :
-  envs_split true [] Δ = Some (Δ1,Δ2) → Δ1 ⊢ Q → Δ ⊢ Q.
-Proof. intros. by rewrite envs_split_sound // sep_elim_l. Qed.
+Lemma tac_clear_spatial Δ Δ' Q :
+  envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q.
+Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
 Lemma tac_duplicate Δ Δ' i p j P Q :
   envs_lookup i Δ = Some (p, P) →
@@ -329,14 +350,16 @@ Lemma tac_next Δ Δ' Q Q' :
 Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
 
 Lemma tac_löb Δ Δ' i Q :
-  envs_persistent Δ = true →
-  envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
+  envs_app true (Esnoc Enil i
+    (▷ env_fold uPred_wand Q (env_spatial Δ)))%I Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
-  rewrite right_id -{2}(always_elim Q) -(löb (□ Q)); apply impl_intro_l.
-  rewrite -always_later -{1}(always_always (□ (▷ Q))) always_and_sep_l'.
-  by rewrite -always_sep wand_elim_r HQ.
+  intros ? HQ. rewrite /of_envs assoc. apply wand_elim_l'.
+  rewrite -(always_elim (_ -★ Q))%I -(löb (□ (_ -★ _)))%I; apply impl_intro_l.
+  apply (always_intro _ _), wand_intro_r.
+  rewrite always_and_sep_l -(assoc _ (▷ _))%I -(assoc _ (■ _))%I -of_envs_def.
+  rewrite envs_app_sound //; simpl; rewrite right_id env_fold_wand HQ.
+  by rewrite -always_later wand_elim_r.
 Qed.
 
 (** * Always *)

proofmode/environments.v

@@ -32,6 +32,12 @@ Instance env_dom {A} : Dom (env A) stringset :=
   fix go Γ := let _ : Dom _ _ := @go in
   match Γ with Enil => ∅ | Esnoc Γ i _ => {[ i ]} ∪ dom stringset Γ end.
 
+Fixpoint env_fold {A B} (f : B → A → A) (x : A) (Γ : env B) : A :=
+  match Γ with
+  | Enil => x
+  | Esnoc Γ _ y => env_fold f (f y x) Γ
+  end.
+
 Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
   match Γapp with
   | Enil => Some Γ

proofmode/pviewshifts.v

@@ -81,7 +81,6 @@ Proof.
   eauto using tac_pvs_timeless.
 Qed.
 
-Hint Immediate env_special_nil_persistent : typeclass_instances.
 Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
   FSASplit Q E fsa fsaV Φ →
   envs_split lr js Δ = Some (Δ1,Δ2) →

proofmode/tactics.v

@@ -4,7 +4,7 @@ From iris.proofmode Require Export notation.
 From iris.prelude Require Import stringmap.
 
 Declare Reduction env_cbv := cbv [
-  env_lookup env_lookup_delete env_delete env_app
+  env_lookup env_fold env_lookup_delete env_delete env_app
     env_replace env_split_go env_split
   decide (* operational classes *)
   sumbool_rec sumbool_rect (* sumbool *)
@@ -755,8 +755,7 @@ Tactic Notation "iNext":=
 
 Tactic Notation "iLöb" "as" constr (H) :=
   eapply tac_löb with _ H;
-    [reflexivity || fail "iLöb: non-empty spatial context"
-    |env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
+    [env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
 
 Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (H) :=
   iRevert { x1 }; iLöb as H; iIntros { x1 }.

tests/heap_lang.v

@@ -42,7 +42,7 @@ Section LiftingTests.
     n1 < n2 →
     Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
-    iIntros {Hn} "HΦ". iLöb {n1 Hn} "HΦ" as "IH".
+    iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - iApply "IH" "% HΦ". omega.
     - iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.