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

Question

我正在尝试编写如下所示的 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 *)

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

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

Answer 1

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

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