結合兩個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。

另一個（不是很方便）的方式將

assert B as h3 by exact (h h2). 

這是什麼pose proof變種相當於。

此外，在一個簡單的情況下，像下面這樣，就可以解決你的目標，而不會引入新的假設：

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