두 개의 Coq 가설을 결합합니다.

Question

두 가지 가설이 있습니다. 하나는 h : A -> B이고 다른 하나는 h2 : A입니다. 가설에 h3 : B이 나타나게하려면 어떻게해야합니까? 새로운 가설로

Answer 1

pose proof (h h2) as h3. 

소개합니다 h3 : B,

specialize (h h2). 

이 h : A -> B h : B로 수정 -이 나중에 h이 필요하지 않을 경우 유용 할 대칭 수

apply h in h2. 

h2 : A을 h2 : B으로 변환합니다.

또 다른 (매우 편리하지) 방법은 pose proof 변종에 해당 무엇

assert B as h3 by exact (h h2). 

하는 것입니다. 또한

, 다음과 같은 간단한 경우에, 당신은 새로운 가설을 도입하여 목표를 해결할 수 있습니다 : 빠른 답변

Goal forall (A B : Prop), (A -> B) -> A -> B. 
    intros A B h h2. 
    apply (h h2). 
Qed.