为什么记忆策略不像记录的那样起作用？

Question

在交互式证明中，我试图将表达式提取到新变量中，同时将相等性捕获为新证明项。

remember 策略似乎就是为此目的而设计的。由于我喜欢为引入的名称指定显式名称，因此我更愿意使用此变体：

remember term as ident eqn:ident

This behaves as remember term as ident, except that the name of the generated equality is also given.

然而，当我尝试它（或其他记住的变体）时，我只得到这个错误：

> remember (prefix ++ suffix) as the_environment eqn:H_prefix_suffix.
>                                                ^^^
Syntax error: 'in' '|-' expected after [prim:ident] (in [tactic:simple_tactic]).

注意错误消息，唯一似乎有效的变体是

remember (prefix ++ suffix) as the_environment in |-.

...不幸的是，它不允许我选择引入的等式证明的名称。

为什么记录的 remember 变体似乎不起作用？

我正在使用 coq 8.4pl6。

Answer 1

我搬起石头砸自己的脚

我之前已经用这种语法声明了一个策略：

Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=
  let x := fresh x in
  let H := fresh "Heq" x in
  (set (x := c); assert (H : x = c) by reflexivity; clearbody x).

这个明确的定义似乎掩盖了内置变体。删除此定义会使其他定义再次可见。

为什么记忆策略不像记录的那样起作用？

Why don't the remember tactics work as documented?

coq