Coq : 하나의 가설을 다른 사람에게 적용하는 방법

Question

문맥 상 두 가지 가설, 즉 a_b : A -> B과 a : A이 있다고 가정합니다. 나는 가설을 더 얻기 위해 a_b을 a에 적용 할 수 있어야한다. b : B. 다음과 같은 상태를 주어

:

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
______________________________________(1/1) 
C 

어떤 전술, foo (a_b a)는 다음과 같은 상태로이 변환이 있어야한다 :

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
b : B 
______________________________________(1/1) 
C 

하지만 무엇 foo을 모르는 입니다.

assert B as b. 
apply a_b. 
exact a. 

그러나 이것은 오히려 역풍, 그리고 좀 더 큰 표현을 심하게하는 경우 대신 a_b a 확장 : 내가 할 수있는

것은 이것이다. 내가 할 수있는

또 다른 한가지는 다음과 같습니다

specialize (a_b a). 

하지만 은에게 내가하고 싶지 않은 a_b 가설을 대체합니다.

Answer 1

pose proof (a_b a) as B. 

원하는대로해야합니다.