检查返回值的策略中的 evar

Question

我正在尝试编写一个返回值的策略，在此过程中需要检查某些内容是否是 evar。

不幸的是，我无法使用is_evar，因为这样该策略不被视为返回值（而是另一种策略）。下面是一个例子。

有什么建议么？

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => is_evar e; 
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

Answer 1

有一个巧妙（或令人讨厌）的小技巧，您可以使用它在 Coq >= 8.5 中将策略执行插入到 constr 构造中：将其包装在match goal.

Ltac reify_wrt 值 ls :=
  将 ls 与
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := 查找 a 中的值
                 让 idx := reify_wrt 值 ls' in
                 构造:(i::idx)
  | ?e :: ?ls' => let check := 匹配目标与 _ => is_evar e 结尾
                  让 i := constr:(100) 进入
                  让 idx := reify_wrt 值 ls' in
                  构造:(i::idx)
  结尾。

因为编程语言奥秘让我着迷，所以我现在将告诉您有关 Ltac 当前和过去的执行模型的更多信息，这些内容可能超出您想了解的内容。

策略评估有两个阶段：策略表达评估和策略运行。在策略运行过程中，会执行排序、细化、重写等操作。在策略表达式评估期间，如果在策略表达的头部位置找到以下结构，则评估以下结构：

• 策略调用已解决/遵循/内联/展开
• let ... in ...将其参数的表达式求值绑定到名称，并进行替换
• constr:(...)进行评估和类型检查
• lazymaytch ... with ... end被求值（使用回溯），并返回成功表达式求值的第一个匹配分支
• match ... with ... end被评估（通过回溯）并且分支被急切地执行。请注意，在这张图中，match很奇怪，因为它迫使战术提前执行。如果您在 Coq < 8.5 中见过“本地定义中不允许的立即匹配生成策略”，那么这是一条错误消息，明确禁止我在上面利用的行为。我猜这是因为这种奇怪的行为match是实现 Ltac 的原始开发人员想要隐藏的一个缺陷。因此，在 Coq 8.4 中，您唯一能注意到它的地方是，如果您坚持match在内部lazymatch并尝试失败级别，并且会注意到，当您通常期望它失败时，它将lazymatch在内部策略执行失败时进行回溯。match

在 Coq 8.5 中，策略引擎被重写以处理相关子目标。这导致了语义上的微妙变化，;只有在使用多个目标之间共享的 evar 时才能观察到这种变化。在重写中，开发人员将 的语义更改lazymatch为“match不回溯”，并取消了对“立即匹配产生策略”的限制。因此你可以做一些奇怪的事情，比如：

let dummy := match goal with _ => rewrite H end in
constr:(true)

并具有产生副作用的构造策略。但是，您不能再执行以下操作：

let tac := lazymatch b with
                | true => tac1
                | false => tac2
                end in
tac long args.

因为在 Coq >= 8.5 中，lazymatch也急切地评估它的分支。