From 24e1a3c7c28d14623e5cb8570d6112c496eeeee9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Fri, 10 Sep 2021 10:47:45 +0200
Subject: [PATCH] Optimize iDestruct IIntuitionistic/ISpatial/IModalElim cases

Following up on the previous commit, this slightly generalizes the
lemmas associated to the intuitionistic/spatial/modalelim cases of
iDestruct to support renaming on the fly, and use these to save a
later renaming.
---
 iris/proofmode/coq_tactics.v  | 12 +++----
 iris/proofmode/ltac_tactics.v | 67 +++++++++++++++++++++++------------
 2 files changed, 50 insertions(+), 29 deletions(-)

diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index ab186a294..3e8effac7 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -174,11 +174,11 @@ 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 j p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  match envs_replace i p true (Esnoc Enil i P') Δ with
+  match envs_replace i p true (Esnoc Enil j P') Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q
   end →
@@ -196,10 +196,10 @@ Proof.
         absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
-Lemma tac_spatial Δ i p P P' Q :
+Lemma tac_spatial Δ i j p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   (if p then FromAffinely P' P else TCEq P' P) →
-  match envs_replace i p false (Esnoc Enil i P') Δ with
+  match envs_replace i p false (Esnoc Enil j P') Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q
   end →
@@ -748,11 +748,11 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_elim Δ i p p' φ P' P Q Q' :
+Lemma tac_modal_elim Δ i j p p' φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal φ p p' P P' Q Q' →
   φ →
-  match envs_replace i p p' (Esnoc Enil i P') Δ with
+  match envs_replace i p p' (Esnoc Enil j P') Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q'
   end →
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 3c5bf6a53..41453a3a7 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -324,8 +324,8 @@ Tactic Notation "iAssumption" :=
 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) *)
+Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=
+  eapply tac_intuitionistic with H H' _ _ _; (* (i:=H) (j:=H') *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iIntuitionistic:" H "not found"
@@ -335,15 +335,27 @@ 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_reduce].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let H' := pretty_ident H' in
+       fail "iIntuitionistic:" H' "not fresh"
+     | _ => idtac (* subgoal *)
+     end].
 
-Local Tactic Notation "iSpatial" constr(H) :=
-  eapply tac_spatial with H _ _ _;
+Local Tactic Notation "iSpatial" constr(H) "as" constr(H') :=
+  eapply tac_spatial with H H' _ _ _;
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iSpatial:" H "not found"
     |pm_reduce; iSolveTC
-    |pm_reduce].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let H' := pretty_ident H' in
+       fail "iSpatial:" H' "not fresh"
+     | _ => idtac (* subgoal *)
+     end].
 
 Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with H _ _ _; (* (i:=H1) *)
@@ -1442,15 +1454,21 @@ Tactic Notation "iNext" open_constr(n) := iModIntro (â–·^n _)%I.
 Tactic Notation "iNext" := iModIntro (â–·^_ _)%I.
 
 (** * Update modality *)
-Tactic Notation "iModCore" constr(H) :=
-  eapply tac_modal_elim with H _ _ _ _ _ _;
+Tactic Notation "iModCore" constr(H) "as" constr(H') :=
+  eapply tac_modal_elim with H H' _ _ _ _ _ _;
     [pm_reflexivity || fail "iMod:" H "not found"
     |iSolveTC ||
      let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
      let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
      fail "iMod: cannot eliminate modality" P "in" Q
     |iSolveSideCondition
-    |pm_reduce; pm_prettify(* subgoal *)].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let H' := pretty_ident H' in
+       fail "iMod:" H' "not fresh"
+     | _ => pm_prettify(* subgoal *)
+     end].
 
 (** * Basic destruct tactic *)
 
@@ -1548,11 +1566,14 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
   | IIntuitionistic ?pat =>
-    iIntuitionistic Hz; iDestructHypGo Hz pat0 pat
+    let x := ident_for_pat_default pat Hz in
+    iIntuitionistic Hz as x; iDestructHypGo x pat0 pat
   | ISpatial ?pat =>
-    iSpatial Hz; iDestructHypGo Hz pat0 pat
+    let x := ident_for_pat_default pat Hz in
+    iSpatial Hz as x; iDestructHypGo x pat0 pat
   | IModalElim ?pat =>
-    iModCore Hz; iDestructHypGo Hz pat0 pat
+    let x := ident_for_pat_default pat Hz in
+    iModCore Hz as x; iDestructHypGo x pat0 pat
   | _ => fail "iDestruct:" pat0 "is not supported due to" pat
   end.
 Local Ltac iDestructHypFindPat Hgo pat found pats :=
@@ -2940,48 +2961,48 @@ Ltac iSimplifyEq := repeat (
 
 (** * Update modality *)
 Tactic Notation "iMod" open_constr(lem) :=
-  iDestructCore lem as false (fun H => iModCore H).
+  iDestructCore lem as false (fun H => iModCore H as H).
 Tactic Notation "iMod" open_constr(lem) "as" constr(pat) :=
-  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as pat).
+  iDestructCore lem as false (fun H => iModCore H as H; last iDestructHyp H as pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
     constr(pat) :=
-  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 ) pat).
+  iDestructCore lem as false (fun H => iModCore H as H; last iDestructHyp H as ( x1 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) :=
-  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 ) pat).
+  iDestructCore lem as false (fun H => iModCore H as H; last iDestructHyp H as ( x1 x2 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
-  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
+  iDestructCore lem as false (fun H => iModCore H as H; last iDestructHyp H as ( x1 x2 x3 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) :=
   iDestructCore lem as false (fun H =>
-    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+    iModCore H as H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) ")" constr(pat) :=
   iDestructCore lem as false (fun H =>
-    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+    iModCore H as H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
   iDestructCore lem as false (fun H =>
-    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+    iModCore H as H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
     constr(pat) :=
   iDestructCore lem as false (fun H =>
-    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+    iModCore H as H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
 Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
     simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
     simple_intropattern(x8) ")" constr(pat) :=
   iDestructCore lem as false (fun H =>
-    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+    iModCore H as H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
 
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
-  iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
+  iDestructCore lem as false (fun H => iModCore H as H; iPure H as pat).
 
 (** * Invariant *)
 
-- 
GitLab