Эквивалент `запомнить (f x) как y eqn:H; clear H; clear x"?

Иногда у меня есть доказательство, которое лучше всего сделать, проецируя в другое пространство. В данный момент я делаю следующее: 

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.

В чем тут проблема?

1 2
coq

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.
5