`remember（f x）と等価です。y eqn：H; Hをクリアする。クリアx？

Question

時には私は、別の空間に投影することによって最もよく行われる証拠を持っています。私は、次の操作を行い、現時点では：

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

しかし、私は次のエラーを取得する：

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

私はLTACでこれを自動化しようとした

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. 

あなたが使用しない方程式を生成しているので、交換する方が良いremembergeneralizeと：

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. 

を使用することができます。例えば、2つの自由変数を持つ式と似たようなことをしたいのであれば、書くだけでよいでしょう。

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