结合两个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.