From 331f96f797144127679cbaba75ceab0b1d6a3557 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Aug 2023 15:56:17 +0200
Subject: [PATCH] Address review feedback.
---
iris/proofmode/base.v | 10 +++++-----
iris/proofmode/ltac_tactics.v | 8 ++++++++
2 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 8144fc887..e918c6bac 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -8,14 +8,14 @@ From Ltac2 Require Ltac2.
(** ** N-ary tactics *)
(** Ltac1 does not provide primitives to manipulate lists (e.g., [ident_list],
-[simple_intropattern_list], needed for [iIntros], [iDestruct], etc. We can do
+[simple_intropattern_list]), needed for [iIntros], [iDestruct], etc. We can do
that in Ltac2. For most proofmode tactics we only need to iterate over a list
(either in forward or backward direction). The Ltac1 tactics [ltac1_list_iter]
and [ltac1_list_rev_iter] allow us to do that while encapsulating the Ltac2
code. These tactics can be used as:
Ltac _iTactic xs :=
- ltac1_list_rev_iter ltac:(fun x => /* stuff */) xs.
+ ltac1_list_iter ltac:(fun x => /* stuff */) xs.
Tactic Notation "iTactic" "(" ne_ident_list(xs) ")" :=
_iTactic xs.
@@ -48,9 +48,9 @@ Ltac ltac1_list_rev_iter tac l :=
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]:
+no nice way to produce an empty list in ltac1. 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)
*)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 00497ab83..3d3ab1058 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2023,6 +2023,14 @@ Ltac _iDestructAccAndHyp0 pat x H :=
| _ => fail "Missing intro pattern for accessor variable"
end.
+(** [_iDestructAccAndHyp xs pat x H] expects [x] to be a variable in the context.
+Then it behaves as follows:
+- If [x] has type [unit], it destructs [x] and continues as
+ [_iDestructHyp H xs pat]. That is, it is basically as if [x] did not exist.
+- Otherwise, [xs] must be a non-empty list of patterns, and the first pattern is
+ applied to [x]. Then we continue as [_iDestructHyp H (tail xs) pat].
+ Basically it is as if "H" (the hypothesis being destructed) actually was
+ [∃ x, H], so that the first pattern in the [xs] destructs this existential. *)
Ltac _iDestructAccAndHyp xs pat x H :=
let go := ltac2:(tac xs |-
match of_ltac1_list xs with
--
GitLab