是否可以将上下文模式转换为 Gallina 函数?

Question

在Ltac中，上下文模式可用于构建Ltac级函数，该函数接受Gallina项并通过填充孔来构造Gallina项。我想具体化这个函数并在 Gallina 级别使用它，而不是 Ltac。

例如，以下代码使用元变量而不是上下文模式工作。

Variables 
(A : Set)
(P : A -> Prop)
(a : A)
(H : forall Q: A -> Prop, Q a).

Goal (P a).
match goal with
| |- ?P a => exact (H P)
end.
Qed.

但是下面的代码不起作用，因为我无法在填写模式之前将变量x带入范围：

Goal (P a).
match goal with
| |- context C[a] => let y := context C[x] in exact (H (fun x => y))
end.
(* The reference x was not found in the current
environment. *)

以下方法也不起作用，因为我无法在 Gallina 中使用 Ltac：

Goal (P a).
match goal with
| |- context C[a] => let y := exact (H (fun x => context C[x]))
end.
(* Syntax error... *)

但是下面的代码表明我的上下文模式的工作方式与我认为应该的那样：

Goal (P a).
match goal with
| |- context C[a] => let y := context C[a] in idtac y
end.
(* (P a) *)

虽然此示例很简单，因为目标是单个应用程序，但通常我希望使用上下文模式来匹配更复杂的目标，然后使用这些模式来构建 Gallina 函数。这能做到吗？

Answer 1

使用ltac:(...)

match goal with
| |- context C[a] => exact (H (fun x => ltac:(let y := context C[x] in exact y)))
end.

ltac:(...)可以取代任何加利纳术语。该洞的预期类型成为包含的策略表达式的目标，执行该表达式以生成新的加利纳项来填充洞。