0

在 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 函数。这可以做到吗？

4

1 回答 1

2

利用ltac:(...)

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

ltac:(...)可以替换任何 Gallina 术语。该漏洞的预期类型成为包含的策略表达式的目标，执行该表达式以生成一个新的 Gallina 术语来填充该漏洞。

于 2020-02-09T03:08:27.070 回答