相当于`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.

这是什么问题？

Answer 1

我假设你试图像这样称呼你的策略:

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.