本文介绍了结合两个Coq假设的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
所以我有两个假设，一个是 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假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！