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