coq - 相当于`remember (fx) as y eqn:H; 清除 H; 清除 x`?

Question

有时我有一个最好通过投影到不同空间来完成的证明。目前，我执行以下操作：

remember (f x) as y eqn:H; clear H; clear x.

我试图用 Ltac 自动化这个：

Ltac project x y :=
  let z := fresh in
    remember x as y eqn:z; clear z; clear x.

但我收到以下错误：

Error: Ltac variable x is bound to f x which cannot be coerced to a variable.

这里有什么问题？

score 5 · Accepted Answer

我假设您正在尝试这样称呼您的策略：

project (f x) y.

如果你展开你给出的定义，你会看到这个调用以

clear (f x).

这个调用是罪魁祸首：你只能清除变量，而不是任意表达式。这是一个可能的修复。

Ltac project x y :=
  match x with
  | ?f ?x' => 
    let z := fresh in
    remember x as y eqn:z; clear z; clear x'
  end.

由于您正在生成一个从未使用过的方程，因此最好替换remember为generalize：

Ltac project x y :=
  match x with
  | ?f ?x' => generalize x; clear x'; intros y
  end.

您也可以考虑使用ssreflect证明语言，它大大简化了这种上下文操作。而不是调用project (f x) y，我们可以使用

 move: (f x)=> {x} y.

这要灵活得多。例如，如果你想用两个自由变量的表达式做类似的事情，你只需要写

move: (f x1 x2)=> {x1 x2} y.

1 回答 1