Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iris

theories/proofmode/coq_tactics.v

@@ -61,17 +61,17 @@ 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,Δ') →
+Lemma tac_assumption Δ i p P Q :
+  envs_lookup i Δ = Some (p,P) →
   FromAssumption p P Q →
-  (if env_spatial_is_nil Δ' then TCTrue
+  (let Δ' := envs_delete true i p Δ in
+   if env_spatial_is_nil Δ' then TCTrue
    else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
   envs_entails Δ Q.
 Proof.
-  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
-  destruct (env_spatial_is_nil Δ') eqn:?.
-  - by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
+  intros ?? H. rewrite envs_entails_eq envs_lookup_sound //.
+  simpl in *. destruct (env_spatial_is_nil _) eqn:?.
+  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
@@ -88,15 +88,14 @@ Proof.
   by rewrite wand_elim_r.
 Qed.
 
-(* TODO: convert to not take Δ' *)
-Lemma tac_clear Δ Δ' i p P Q :
-  envs_lookup_delete true i Δ = Some (p,P,Δ') →
+Lemma tac_clear Δ i p P Q :
+  envs_lookup i Δ = Some (p,P) →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  envs_entails Δ' Q →
+  envs_entails (envs_delete true i p Δ) Q →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
-  by destruct p; rewrite /= HQ sep_elim_r.
+  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
+  by destruct p; rewrite /= sep_elim_r.
 Qed.
 
 (** * False *)
@@ -124,15 +123,14 @@ 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, Δ') →
+Lemma tac_pure Δ i p P φ Q :
+  envs_lookup i Δ = Some (p, P) →
   IntoPure P φ →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  (φ → envs_entails Δ' Q) → envs_entails Δ Q.
+  (φ → envs_entails (envs_delete true i p Δ) Q) → envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq=> ?? HPQ HQ.
-  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
+  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
   - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
     by apply pure_elim_l.
   - destruct HPQ.
@@ -252,9 +250,9 @@ 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 Δ' *)
-Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
-  envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
+Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
+  envs_lookup i Δ = Some (p, P1) →
+  let Δ' := envs_delete remove_intuitionistic i p Δ in
   envs_lookup j Δ' = Some (q, R) →
   IntoWand q p R P1 P2 →
   match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
@@ -262,8 +260,7 @@ Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /IntoWand.
-  intros [? ->]%envs_lookup_delete_Some ? HR ?.
+  rewrite envs_entails_eq /IntoWand. intros ?? HR ?.
   destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
   rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
@@ -273,15 +270,24 @@ Proof.
   - by rewrite HR assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
+Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
+  envs_lookup j Δ = Some (q, R) →
   IntoWand q false R P1 P2 → AddModal P1' P1 Q →
-  (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
+  match
+    ''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
+    js (envs_delete true j q Δ);
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
-    Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
+    Some (Δ1,Δ2') (* does not preserve position of [j] *)
+  with
+  | Some (Δ1,Δ2') =>
+     (* The constructor [conj] of [∧] still stores the contexts [Δ1] and [Δ2'] *)
+     envs_entails Δ1 P1' ∧ envs_entails Δ2' Q
+  | None => False
+  end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
+  rewrite envs_entails_eq. intros ??? HQ.
+  destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
+  destruct HQ as [HP1 HQ].
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
@@ -297,15 +303,15 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
-Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
+Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
+  envs_lookup j Δ = Some (q, R) →
   IntoWand q false R P1 P2 →
   AddModal P1' P1 Q →
-  envs_entails Δ' (P1' ∗ locked Q') →
+  envs_entails (envs_delete true j q Δ) (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  rewrite envs_entails_eq. intros ??? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
@@ -330,18 +336,18 @@ Proof.
   by rewrite intuitionistically_emp left_id wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_intuitionistic Δ Δ' j q P1 P1' P2 R Q :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
+Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
+  envs_lookup j Δ = Some (q, R) →
   IntoWand q true R P1 P2 →
   Persistent P1 →
   IntoAbsorbingly P1' P1 →
-  envs_entails Δ' P1' →
+  envs_entails (envs_delete true j q Δ) P1' →
   match envs_simple_replace j q (Esnoc Enil j P2) Δ with
   | Some Δ'' => envs_entails Δ'' Q
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ??? HP1 HQ.
+  rewrite envs_entails_eq => ???? HP1 HQ.
   destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite -HQ envs_lookup_sound //.
   rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
@@ -464,12 +470,12 @@ Proof.
   by rewrite wand_elim_r.
 Qed.
 
-Lemma tac_apply Δ Δ' i p R P1 P2 :
-  envs_lookup_delete true i Δ = Some (p, R, Δ') →
+Lemma tac_apply Δ i p R P1 P2 :
+  envs_lookup i Δ = Some (p, R) →
   IntoWand p false R P1 P2 →
-  envs_entails Δ' P1 → envs_entails Δ P2.
+  envs_entails (envs_delete true i p Δ) P1 → envs_entails Δ P2.
 Proof.
-  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
+  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_sound //.
   by rewrite (into_wand p false) /= HP1 wand_elim_l.
 Qed.
 
@@ -570,12 +576,12 @@ Proof.
   auto using and_intro, pure_intro.
 Qed.
 
-Lemma tac_frame Δ Δ' i p R P Q :
-  envs_lookup_delete false i Δ = Some (p, R, Δ') →
+Lemma tac_frame Δ i p R P Q :
+  envs_lookup i Δ = Some (p, R) →
   Frame p R P Q →
-  envs_entails Δ' Q → envs_entails Δ P.
+  envs_entails (envs_delete false i p Δ) Q → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
+  rewrite envs_entails_eq. intros ? Hframe HQ.
   rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
 Qed.
 
@@ -686,9 +692,9 @@ Proof.
 Qed.
 
 (** * Invariants *)
-Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X → PROP))
+Lemma tac_inv_elim {X : Type} Δ i j φ p Pinv Pin Pout (Pclose : option (X → PROP))
       Q (Q' : X → PROP) :
-  envs_lookup_delete false i Δ = Some (p, Pinv, Δ') →
+  envs_lookup i Δ = Some (p, Pinv) →
   ElimInv φ Pinv Pin Pout Pclose Q Q' →
   φ →
   (∀ R,
@@ -696,11 +702,11 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
       (Pin -∗
        (∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x) -∗
        R
-      )%I) Δ'
+      )%I) (envs_delete false i p Δ)
     with Some Δ'' => envs_entails Δ'' R | None => False end) →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) Hmatch.
+  rewrite envs_entails_eq=> ? Hinv ? /(_ Q) Hmatch.
   destruct (envs_app _ _ _) eqn:?; last done.
   rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.

theories/proofmode/ltac_tactics.v

@@ -172,7 +172,7 @@ Ltac iElaborateSelPat pat :=
   end.
 
 Local Ltac iClearHyp H :=
-  eapply tac_clear with _ H _ _; (* (i:=H) *)
+  eapply tac_clear with H _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iClear:" H "not found"
@@ -180,7 +180,7 @@ Local Ltac iClearHyp H :=
      let H := pretty_ident H in
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iClear:" H ":" P "not affine and the goal not absorbing"
-    |].
+    |pm_reduce].
 
 Local Ltac iClear_go Hs :=
   lazymatch Hs with
@@ -228,7 +228,7 @@ Ltac, but it may be possible in Ltac2. *)
 
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
-  eapply tac_assumption with _ H _ _; (* (i:=H) *)
+  eapply tac_assumption with H _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iExact:" H "not found"
@@ -262,7 +262,7 @@ Tactic Notation "iAssumption" :=
     lazymatch Γ with
     | Esnoc ?Γ ?j ?P => first
        [pose proof (_ : FromAssumption p P Q) as Hass;
-        eapply (tac_assumption _ _ j p P);
+        eapply (tac_assumption _ j p P);
           [pm_reflexivity
           |apply Hass
           |pm_reduce; iSolveTC ||
@@ -297,7 +297,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
     |pm_reduce].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
-  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
+  eapply tac_pure with H _ _ _; (* (i:=H1) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iPure:" H "not found"
@@ -307,7 +307,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
     |pm_reduce; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iPure:" P "not affine and the goal not absorbing"
-    |intros pat].
+    |pm_reduce; intros pat].
 
 Tactic Notation "iEmpIntro" :=
   iStartProof;
@@ -342,14 +342,14 @@ Local Ltac iFramePure t :=
 
 Local Ltac iFrameHyp H :=
   iStartProof;
-  eapply tac_frame with _ H _ _ _;
+  eapply tac_frame with H _ _ _;
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iFrame:" H "not found"
     |iSolveTC ||
      let R := match goal with |- Frame _ ?R _ _ => R end in
      fail "iFrame: cannot frame" R
-    |iFrameFinish].
+    |pm_reduce; iFrameFinish].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.
@@ -784,7 +784,7 @@ Ltac iSpecializePat_go H1 pats :=
     | SIdent ?H2 [] :: ?pats =>
        (* If we not need to specialize [H2] we can avoid a lot of unncessary
        context manipulation. *)
-       notypeclasses refine (tac_specialize false _ _ H2 _ H1 _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize false _ H2 _ H1 _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H2 := pretty_ident H2 in
           fail "iSpecialize:" H2 "not found"
@@ -811,7 +811,7 @@ Ltac iSpecializePat_go H1 pats :=
          Ltac backtraces (which would otherwise include the whole closure). *)
          [.. (* side-conditions of [iSpecialize] *)
          |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
-          notypeclasses refine (tac_specialize true _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
+          notypeclasses refine (tac_specialize true _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
             [pm_reflexivity ||
              let H2tmp := pretty_ident H2tmp in
              fail "iSpecialize:" H2tmp "not found"
@@ -836,7 +836,7 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce;
           iSpecializePat_go H1 pats]
     | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -845,13 +845,13 @@ Ltac iSpecializePat_go H1 pats :=
           let Q := match goal with |- Persistent ?Q => Q end in
           fail "iSpecialize:" Q "not persistent"
          |iSolveTC
-         |iFrame Hs_frame; solve_done d (*goal*)
+         |pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
          |pm_reduce; iSpecializePat_go H1 pats]
     | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
        fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-       notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -860,13 +860,18 @@ Ltac iSpecializePat_go H1 pats :=
           | GSpatial => class_apply add_modal_id
           | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
           end
-         |pm_reflexivity ||
-          let Hs' := iMissingHyps Hs' in
-          fail "iSpecialize: hypotheses" Hs' "not found"
-         |iFrame Hs_frame; solve_done d (*goal*)
-         |iSpecializePat_go H1 pats]
+         |pm_reduce;
+          lazymatch goal with
+          | |- False =>
+            let Hs' := iMissingHyps Hs' in
+            fail "iSpecialize: hypotheses" Hs' "not found"
+          | _ =>
+            split;
+              [iFrame Hs_frame; solve_done d (*goal*)
+              |iSpecializePat_go H1 pats]
+          end]
     | SAutoFrame GIntuitionistic :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -874,10 +879,10 @@ Ltac iSpecializePat_go H1 pats :=
          |iSolveTC ||
           let Q := match goal with |- Persistent ?Q => Q end in
           fail "iSpecialize:" Q "not persistent"
-         |solve [iFrame "∗ #"]
+         |pm_reduce; solve [iFrame "∗ #"]
          |pm_reduce; iSpecializePat_go H1 pats]
     | SAutoFrame ?m :: ?pats =>
-       notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_frame _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -886,7 +891,8 @@ Ltac iSpecializePat_go H1 pats :=
           | GSpatial => class_apply add_modal_id
           | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
           end
-         |first
+         |pm_reduce;
+          first
             [notypeclasses refine (tac_unlock_emp _ _ _)
             |notypeclasses refine (tac_unlock_True _ _ _)
             |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
@@ -1050,7 +1056,7 @@ premises [n], the tactic will have the following behavior:
 actual error. *)
 Local Ltac iApplyHypExact H :=
   first
-    [eapply tac_assumption with _ H _ _; (* (i:=H) *)
+    [eapply tac_assumption with H _ _; (* (i:=H) *)
        [pm_reflexivity || fail 1
        |iSolveTC || fail 1
        |pm_reduce; iSolveTC]
@@ -1060,10 +1066,11 @@ Local Ltac iApplyHypExact H :=
      end].
 Local Ltac iApplyHypLoop H :=
   first
-    [eapply tac_apply with _ H _ _ _;
+    [eapply tac_apply with H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_prettify (* reduce redexes created by instantiation *)]
+      |pm_reduce;
+       pm_prettify (* reduce redexes created by instantiation *)]
     |iSpecializePat H "[]"; last iApplyHypLoop H].
 
 Tactic Notation "iApplyHyp" constr(H) :=
@@ -2299,7 +2306,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
       first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
     end in
   lazymatch goal with
-  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some _ =>
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some _ =>
      first [find Γp i|find Γs i]; pm_reflexivity
   end.