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