Ltac：将目标与取决于先前目标名称的类型匹配答案

【问题标题】：Ltac: Matching goal with type that depends on name of previous goalLtac：将目标与取决于先前目标名称的类型匹配
【发布时间】：2019-01-07 05:01:56
【问题描述】：

我正在尝试编写如下所示的 Ltac 代码：

match goal with
    | [ e : expr, H : (is_v_of_expr e = true) |- _ ] => idtac
end.
(* The reference e was not found in the current environment *)

问题是，试图匹配上下文中存在值的情况，以及关于该值的一些事实。所以我混合了假设名称和假设类型的命名空间。最终目标是创建一个循环，为上下文中的每个 expr 破坏 (is_v_of_expr e)，但要确保它不会通过不断破坏相同的表达式来循环。

是否可以为这样的事情编写 Ltac 匹配表达式？

【问题讨论】：

【解决方案1】：

您需要使用嵌套匹配。以下应该可以工作。

match goal with
| e : expr |- _ =>
  match goal with
  | H : is_v_of_expr e = true |- _ => idtac
  end
end.

【讨论】：

这是误导。 ?e 隐藏了之前的 e 的名称。如果您执行| [ n : nat, H : ?n = ?n |- _ ]，则不能保证H 等于nats。