Delete extra copies of context from terms for some proof mode tactics.

tests/proofmode.ref

@@ -118,7 +118,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   ============================
   "H1" : ⌜S (S (S x)) = y⌝
   --------------------------------------□
-  "H2" : ⌜(1 + y)%nat = z⌝
+  "H2" : ⌜1 + y = z⌝
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
   
@@ -459,11 +459,13 @@ x is already used.
 "iSplit_one_of_many"
      : string
 The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
-Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+In nested Ltac calls to "iSplitL (constr)" and "iMissingHyps", last call
+failed.
+No matching clauses for match.
 The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
-Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+In nested Ltac calls to "iSplitL (constr)" and "iMissingHyps", last call
+failed.
+No matching clauses for match.
 "iExact_fail"
      : string
 The command has indeed failed with message:
@@ -519,6 +521,7 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
 "iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypFindPat>",

theories/proofmode/coq_tactics.v

@@ -28,13 +28,17 @@ Lemma tac_eval Δ Q Q' :
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
-Lemma tac_eval_in Δ Δ' i p P P' Q :
+Lemma tac_eval_in Δ i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   (∀ (P'':=P'), P ⊢ P') →
-  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /=. intros ? HP ? <-.
+  destruct (envs_simple_replace) as [Δ'|] eqn:Hrep; last (intros; by exfalso).
+  rewrite envs_entails_eq /=. intros ? HP ?.
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite HP wand_elim_r.
 Qed.
@@ -57,6 +61,7 @@ Proof. intros H. induction H; simpl; apply _. Qed.
 Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
 Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete true i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
@@ -70,16 +75,21 @@ Proof.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
-Lemma tac_rename Δ Δ' i j p P Q :
+Lemma tac_rename Δ i j p P Q :
   envs_lookup i Δ = Some (p,P) →
-  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
-  envs_entails Δ' Q →
+  match envs_simple_replace i p (Esnoc Enil j P) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
-  by rewrite wand_elim_r.
+  destruct (envs_simple_replace) as [Δ'|] eqn:Hrep.
+  - rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
+    by rewrite wand_elim_r.
+  - intros; by exfalso.
 Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete true i Δ = Some (p,P,Δ') →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
@@ -115,6 +125,7 @@ Proof.
   - by apply pure_intro.
 Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete true i Δ = Some (p, P, Δ') →
   IntoPure P φ →
@@ -136,14 +147,18 @@ Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → env
 Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Intuitionistic *)
-Lemma tac_intuitionistic Δ Δ' i p P P' Q :
+Lemma tac_intuitionistic Δ i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_replace i p true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
+  destruct (envs_replace) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
+  rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
   destruct p; simpl; rewrite /bi_intuitionistically.
   - by rewrite -(into_persistent true P) /= wand_elim_r.
   - destruct HPQ.
@@ -155,14 +170,18 @@ Proof.
 Qed.
 
 (** * Implication and wand *)
-Lemma tac_impl_intro Δ Δ' i P P' Q R :
+Lemma tac_impl_intro Δ i P P' Q R :
   FromImpl R P Q →
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
-  envs_app false (Esnoc Enil i P') Δ = Some Δ' →
   FromAffinely P' P →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app false (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  destruct (envs_app) eqn:?; last by (intros; exfalso).
+  rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P' P) -affinely_and_lr.
@@ -170,13 +189,17 @@ Proof.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
-Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
+Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
   FromImpl R P Q →
   IntoPersistent false P P' →
-  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromImpl envs_entails_eq => <- ?? <-.
+  destruct (envs_app) eqn:?; last by (intros; exfalso).
+  rewrite /FromImpl envs_entails_eq => <- ??.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
   by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
@@ -187,22 +210,32 @@ Proof.
   rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
 Qed.
 
-Lemma tac_wand_intro Δ Δ' i P Q R :
+Lemma tac_wand_intro Δ i P Q R :
   FromWand R P Q →
-  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  (match envs_app false (Esnoc Enil i P) Δ with
+  | None => False
+  | Some Δ' =>  envs_entails Δ' Q
+   end) →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromWand envs_entails_eq => <- ? HQ.
-  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
+  destruct (envs_app) as [Δ'|] eqn:Hrep.
+  - rewrite /FromWand envs_entails_eq => <- HQ.
+    rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
+  - intros; by exfalso.
 Qed.
-Lemma tac_wand_intro_intuitionistic Δ Δ' i P P' Q R :
+
+Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
   FromWand R P Q →
   IntoPersistent false P P' →
   TCOr (Affine P) (Absorbing Q) →
-  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromWand envs_entails_eq => <- ? HPQ ? HQ.
+  destruct (envs_app) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
+  rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
   rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
@@ -221,6 +254,7 @@ Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
+(* TODO: convert to not take Δ' or Δ'' *)
 Lemma tac_specialize remove_intuitionistic Δ Δ' Δ'' i p j q P1 P2 R Q :
   envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
   envs_lookup j Δ' = Some (q, R) →
@@ -276,14 +310,19 @@ Proof.
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_pure Δ Δ' j q a R P1 P2 φ Q :
+Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q true R P1 P2 →
   FromPure a P1 φ →
-  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
-  φ → envs_entails Δ' Q → envs_entails Δ Q.
+  φ →
+  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
+  destruct envs_simple_replace as [Δ'|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -intuitionistically_if_idemp (into_wand q true) /=.
   rewrite -(from_pure a P1) pure_True //.
   rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
@@ -369,29 +408,41 @@ Proof.
   rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
 Qed.
 
-Lemma tac_assert Δ Δ' j P Q :
-  envs_app true (Esnoc Enil j (P -∗ P)%I) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+Lemma tac_assert Δ j P Q :
+  match envs_app true (Esnoc Enil j (P -∗ P)%I) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ? <-. rewrite (envs_app_singleton_sound Δ) //; simpl.
+  destruct (envs_app) as [Δ'|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
   by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
-Lemma tac_pose_proof Δ Δ' j P Q :
+Lemma tac_pose_proof Δ j P Q :
   P →
-  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_app true (Esnoc Enil j P) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => HP ? <-. rewrite envs_app_singleton_sound //=.
+  destruct (envs_app) as [Δ'|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
   by rewrite -HP /= intuitionistically_emp emp_wand.
 Qed.
 
-Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
+Lemma tac_pose_proof_hyp Δ Δ' i p j P Q :
   envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  envs_app p (Esnoc Enil j P) Δ' = Some Δ'' →
-  envs_entails Δ'' Q → envs_entails Δ Q.
+  match envs_app p (Esnoc Enil j P) Δ' with
+  | None => False
+  | Some Δ'' => envs_entails Δ'' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? <-.
+  destruct (envs_app) as [Δ''|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some.
+  intros [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
 Qed.
@@ -411,12 +462,15 @@ Lemma tac_and_split Δ P Q1 Q2 :
 Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Lemma tac_sep_split Δ Δ1 Δ2 d js P Q1 Q2 :
+Lemma tac_sep_split Δ d js P Q1 Q2 :
   FromSep P Q1 Q2 →
-  envs_split d js Δ = Some (Δ1,Δ2) →
-  envs_entails Δ1 Q1 → envs_entails Δ2 Q2 → envs_entails Δ P.
+  match envs_split d js Δ with
+  | None => False
+  | Some (Δ1,Δ2) => envs_entails Δ1 Q1 ∧ envs_entails Δ2 Q2
+  end → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq=>?? HQ1 HQ2.
+  destruct (envs_split) as [(Δ1&Δ2)|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq=>? [HQ1 HQ2].
   rewrite envs_split_sound //. by rewrite HQ1 HQ2.
 Qed.
 
@@ -446,15 +500,20 @@ Proof.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
+Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
   (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
-  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
-  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
-  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
+  destruct (envs_simple_replace) as [Δ'|] eqn:Hrep.
+  - rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
+    * by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
+    * by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
+  - intros; by exfalso.
 Qed.
 
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -487,7 +546,7 @@ Qed.
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq => ?? ->. rewrite -(frame true ⌜φ⌝ P) /=.
+  rewrite envs_entails_eq => ?? ->. rewrite -(frame _ ⌜φ⌝ P) /=.
   rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
@@ -498,7 +557,7 @@ Lemma tac_frame Δ Δ' i p R P Q :
   envs_entails Δ' Q → envs_entails Δ P.
 Proof.
   rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? HQ.
-  rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame p R P) HQ.
+  rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame _ R P) HQ.
 Qed.
 
 (** * Disjunction *)
@@ -513,13 +572,18 @@ Proof.
   rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
 Qed.
 
-Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
+Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoOr P P1 P2 →
-  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
-  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
-  envs_entails Δ1 Q → envs_entails Δ2 Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc Enil j1 P1) Δ,
+        envs_simple_replace i p (Esnoc Enil j2 P2) Δ with
+  | Some Δ1, Some Δ2 => envs_entails Δ1 Q ∧ envs_entails Δ2 Q
+  | _, _ => False
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? HP1 HP2. rewrite envs_lookup_sound //.
+  destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; [| by intros; exfalso].
+  destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; [| by intros; exfalso].
+  rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
   rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
     by rewrite wand_elim_r.
@@ -534,14 +598,17 @@ Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q :
   envs_entails Δ Q.
 Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
 
-Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → PROP) Q :
+Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
   (∃ x : A,
-    envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧
-    envs_entails Δ' Q) →
+      match envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ with
+      | None => False
+      | Some Δ' => envs_entails Δ' Q
+      end) →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ?? (x&?&?).
+  rewrite envs_entails_eq. intros ?? (x&?).
+  destruct (envs_simple_replace) as [Δ'|] eqn:?; [| by exfalso].
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
@@ -572,14 +639,18 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_elim Δ Δ' i p p' φ P' P Q Q' :
+Lemma tac_modal_elim Δ i p p' φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal φ p p' P P' Q Q' →
   φ →
-  envs_replace i p p' (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q' → envs_entails Δ Q.
+  match envs_replace i p p' (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q'
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
+  destruct (envs_replace) as [Δ'|] eqn:?; last by (intros; exfalso).
+  rewrite envs_entails_eq => ??? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ. by eapply elim_modal.
 Qed.
 
@@ -864,15 +935,18 @@ Qed.
 Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
-  ∀ {A : ofeT} Δ' (x y : A) (Φ : A → PROP),
+  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
     IntoInternalEq Pxy x y →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
-    envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
-    envs_entails Δ' Q →
+    match envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ with
+    | None => False
+    | Some Δ' => envs_entails Δ' Q
+    end →
     envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /IntoInternalEq => ?? A Δ' x y Φ HPxy HP ?? <-.
+  rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
+  destruct (envs_simple_replace) as [Δ'|] eqn:?; last by exfalso. rewrite -Hentails.
   rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
   rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.

theories/proofmode/ltac_tactics.v

@@ -119,13 +119,17 @@ Ltac iFresh :=
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
-  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
+  eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
     [pm_reflexivity ||
      let H1 := pretty_ident H1 in
      fail "iRename:" H1 "not found"
-    |pm_reflexivity ||
-     let H2 := pretty_ident H2 in
-     fail "iRename:" H2 "not fresh"|].
+    |pm_reduce;
+     lazymatch goal with
+       | |- False =>
+         let H2 := pretty_ident H2 in
+         fail "iRename:" H2 "not fresh"
+       | _ => idtac (* subogal *)
+     end].
 
 (** Elaborated selection patterns, unlike the type [sel_pat], contains
 only specific identifiers, and no wildcards like `#` (with the
@@ -197,11 +201,10 @@ Local Ltac iEval_go t Hs :=
   | [] => idtac
   | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
   | ESelIdent _ ?H :: ?Hs =>
-    eapply tac_eval_in with _ H _ _ _;
+    eapply tac_eval_in with H _ _ _;
       [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
       |let x := fresh in intros x; t; unfold x; reflexivity
-      |pm_reflexivity
-      |iEval_go t Hs]
+      |pm_reduce; iEval_go t Hs]
   end.
 
 Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
@@ -276,7 +279,7 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
 
 (** * Making hypotheses intuitionistic or pure *)
 Local Tactic Notation "iIntuitionistic" constr(H) :=
-  eapply tac_intuitionistic with _ H _ _ _; (* (i:=H) *)
+  eapply tac_intuitionistic with H _ _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iIntuitionistic:" H "not found"
@@ -286,7 +289,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
     |pm_reduce; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iIntuitionistic:" P "not affine and the goal not absorbing"
-    |pm_reflexivity|].
+    |pm_reduce].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
@@ -448,41 +451,51 @@ Local Tactic Notation "iIntro" constr(H) :=
   iStartProof;
   first
   [(* (?Q → _) *)
-    eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
+    eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
       [iSolveTC
       |pm_reduce; iSolveTC ||
        let P := lazymatch goal with |- Persistent ?P => P end in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
-      |pm_reflexivity ||
-       let H := pretty_ident H in
-       fail 1 "iIntro:" H "not fresh"
       |iSolveTC
-      |(* subgoal *)]
+      |pm_reduce;
+       let H := pretty_ident H in
+        lazymatch goal with
+        | |- False =>
+          let H := pretty_ident H in
+          fail 1 "iIntro:" H "not fresh"
+        | _ => idtac (* subgoal *)
+        end]
   |(* (_ -∗ _) *)
-    eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
+    eapply tac_wand_intro with H _ _; (* (i:=H) *)
       [iSolveTC
-      | pm_reflexivity ||
-        let H := pretty_ident H in
-        fail 1 "iIntro:" H "not fresh"
-      |(* subgoal *)]
+      | pm_reduce;
+        lazymatch goal with
+        | |- False =>
+          let H := pretty_ident H in
+          fail 1 "iIntro:" H "not fresh"
+        | _ => idtac (* subgoal *)
+        end]
   | fail 1 "iIntro: nothing to introduce" ].
 
 Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
   first
   [(* (?P → _) *)
-   eapply tac_impl_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
+   eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
      [iSolveTC
      |iSolveTC ||
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
       fail 1 "iIntro:" P "not persistent"
-     |pm_reflexivity ||
-      let H := pretty_ident H in
-      fail 1 "iIntro:" H "not fresh"
-     |(* subgoal *)]
+     |pm_reduce;
+      lazymatch goal with
+      | |-