2017-11-05 9 views
2

때로는 다른 공간으로 투영하여 가장 좋은 증거가 있습니다.`remember (f x)와 같음 : y eqn : H; H를 맑게하십시오; 명확한 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. 

를? 당신은 당신이 준 정의를 전개하는 경우

project (f x) y. 

, 당신은이 호출이 있습니다이 호출이

clear (f x). 

로 끝나는 것을 볼 수 있습니다 :

답변

5

난 당신이처럼 전술을 호출하려고하는 가정 범인 : 임의의 표현식이 아니라 변수 만 지울 수 있습니다. 가능한 수정이 있습니다.

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. 

를 사용할 수 있습니다. 예를 들어 두 개의 자유 변수가있는 표현식과 비슷한 작업을 원할 경우

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

멋진 답변입니다. 통찰력을 가져 주셔서 대단히 감사합니다. –

+0

@CarlPatenaudePoulin 환영합니다! –