From 0972d9c60cd68d0531c04217674895ad35b9bc00 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 18:00:17 +0200
Subject: [PATCH] Add `with_ltac1_nil`.

---
 iris/proofmode/base.v         | 11 +++++++++++
 iris/proofmode/ltac_tactics.v | 23 ++++++++---------------
 2 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 6b169bdba..db4811a3b 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -47,6 +47,17 @@ Ltac ltac1_list_rev_iter tac l :=
                                       (List.rev (of_ltac1_list l))) in
   go tac l.
 
+(** Since the Ltac1-Ltac2 API only supports unit-returning functions, there is
+no nice way to call [Ltac]s such as [iTactic_] above with the empty list. We
+therefore often define a special version [iTactic0_] for the empty list. This
+version can be created using [with_ltac1_nil]:
+
+  Ltac iTactic0_ := with_ltac1_nil ltac:(fun xs => iTactic_ xs)
+*)
+Ltac with_ltac1_nil tac :=
+  let go := ltac2:(tac |- ltac1:(tac l |- tac l) tac (Ltac1.of_list [])) in
+  go tac.
+
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 40392ef86..0e2b3bfa0 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1761,16 +1761,9 @@ Ltac iHypsContaining x :=
   let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
   let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
-Ltac iInduction0_ x Hs tac IH :=
-  iRevertIntros0_ Hs ltac:(fun _ =>
-    iRevertIntros0_ "∗" ltac:(fun _ =>
-      let Hsx := iHypsContaining x in
-      iRevertIntros0_ Hsx ltac:(fun _ =>
-        iInductionCore tac as IH
-      )
-    )
-  ).
 Ltac iInduction_ x xs Hs tac IH :=
+  (* FIXME: We should be able to do this in a more sane way, by concatenating
+  the spec patterns instead of calling [iRevertIntros] multiple times. *)
   iRevertIntros0_ Hs ltac:(fun _ =>
     iRevertIntros_ xs "∗" ltac:(fun _ =>
       let Hsx := iHypsContaining x in
@@ -1779,6 +1772,8 @@ Ltac iInduction_ x xs Hs tac IH :=
       )
     )
   ).
+Ltac iInduction0_ x Hs tac IH :=
+  with_ltac1_nil ltac:(fun xs => iInduction_ x xs Hs tac IH).
 
 (* Without induction scheme *)
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
@@ -1826,18 +1821,16 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      | _ => idtac
      end].
 
-Ltac iLöb0_ Hs IH :=
-  iRevertIntros0_ Hs ltac:(fun _ =>
-    iRevertIntros0_ "∗" ltac:(fun _ =>
-      iLöbCore as IH
-    )
-  ).
 Ltac iLöb_ xs Hs IH :=
+  (* FIXME: We should be able to do this in a more sane way, by concatenating
+  the spec patterns instead of calling [iRevertIntros] multiple times. *)
   iRevertIntros0_ Hs ltac:(fun _ =>
     iRevertIntros_ xs "∗" ltac:(fun _ =>
       iLöbCore as IH
     )
   ).
+Ltac iLöb0_ Hs IH :=
+  with_ltac1_nil ltac:(fun xs => iLöb_ xs Hs IH).
 
 Tactic Notation "iLöb" "as" constr (IH) :=
   iLöb0_ "" IH.
-- 
GitLab