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

这就是姿势证明变体的等效内容。

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

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