结合两个Coq假设 [英] Combining two Coq hypotheses

问题描述

所以我有两个假设，一个是 h：A-> B ，另一个是 h2：A 。如何使 h3：B 出现在我的假设中？

So I have two hypotheses, one that is h : A -> B, and the other which is h2 : A. How can I get h3 : B to appear in my hypotheses?

推荐答案

pose proof (h h2) as h3.

引入 h3：B 作为新的假设，

specialize (h h2).

修改 h：A-> B 转换为 h：B －如果您不需要 h 之后，对称地，

modifies h : A -> B into h : B -- this can be useful if you won't need h later, and symmetrically,

apply h in h2.

将 h2：A 转换为 h2：B 。

另一种（不是很方便）的方法是

Another (not very convenient) way would be to

assert B as h3 by exact (h h2).

这就是姿势证明的等效形式

此外，在如下所示的简单情况下，您也可以在不引入新假设的情况下解决目标：

Also, in a simple case like the following, you can solve your goal without introducing a new hypothesis:

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

这篇关于结合两个Coq假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！