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

Question

在 Ltac 中，上下文模式可用于构建 Ltac-level 函数，该函数接受 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:(...) 可以替换任何 Gallina 术语。该洞的预期类型成为包含的策略表达式的目标，执行该表达式以生成新的 Gallina 项来填充该洞。

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

Is it possible to turn a context pattern into a Gallina function?

coq

ltac