From 20b0a19dff10a30643bee0a5513a7d1ca277d4ad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Thu, 2 Sep 2021 00:52:06 +0200
Subject: [PATCH] Optimize iIntoEmpValid

With large proof contexts and lemmas with many forall quantifiers,
iIntoEmpValid can become quite slow. This makes it go faster by adding
"fast paths" for the -> and forall cases, gated by Ltac pattern
matching (which is faster than trying to unify with refine and fail).
---
 CHANGELOG.md                  |  3 +++
 iris/proofmode/ltac_tactics.v | 46 ++++++++++++++++++++++++++---------
 2 files changed, 38 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ef8a23a4c..3c06e152d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,9 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Rename the main entry point module for the proofmode from
   `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal
   circumstances, this should be the only proofmode file you need to import.
+* Improve performance of the `iIntoEmpValid` tactic used by `iPoseProof`,
+  especially in the case of large goals and lemmas with many forall quantifiers
+  (by Armaël Guéneau)
 
 **Changes in `bi`:**
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index d9ab16e89..944a0bc67 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -816,17 +816,41 @@ generates a goal [A_i] for each non-dependent argument [x_i : A_i].
 
 For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
 [iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
-[?Q] with [R1 ?x -∗ R2 ?x]. *)
-Ltac iIntoEmpValid_go := first
-  [(* Case [φ → ψ] *)
-   notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
-     [(*goal for [φ] *)|iIntoEmpValid_go]
-  |(* Case [∀ x : A, φ] *)
-   notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
-  |(* Case [∀.. x : TT, φ] *)
-   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
-  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
-   notypeclasses refine (into_emp_valid_here _ _ _)].
+[?Q] with [R1 ?x -∗ R2 ?x].
+
+The tactic is implemented so as to provide a "fast path" for the arrow, forall
+and tforall cases, gated by syntactic ltac pattern matching on the shape of the
+goal. This is an optimization: the behavior of the tactic is equivalent to the
+code in the last "wildcard" case, but faster on larger goals, where running
+(possibly failing) [notypeclasses refine]s can take a significant amount of
+time.
+*)
+Ltac iIntoEmpValid_go :=
+  lazymatch goal with
+  | |- IntoEmpValid (?φ → ?ψ) _ =>
+    (* Case [φ → ψ] *)
+    (* note: the ltac pattern [_ → _] would not work as it would also match
+       [∀ _, _] *)
+    notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
+      [(*goal for [φ] *)|iIntoEmpValid_go]
+  | |- IntoEmpValid (∀ _, _) _ =>
+    (* Case [∀ x : A, φ] *)
+    notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+  | |- IntoEmpValid (∀.. _, _) _ =>
+    (* Case [∀.. x : TT, φ] *)
+    notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
+  | |- _ =>
+    first
+      [(* Case [φ → ψ] *)
+       notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
+         [(*goal for [φ] *)|iIntoEmpValid_go]
+      |(* Case [∀ x : A, φ] *)
+       notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+      |(* Case [∀.. x : TT, φ] *)
+       notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
+      |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
+       notypeclasses refine (into_emp_valid_here _ _ _) ]
+  end.
 
 Ltac iIntoEmpValid :=
   (* Factor out the base case of the loop to avoid needless backtracking *)
-- 
GitLab