文章/答案/技术大牛

发布

社区首页 >问答首页 >如何将引理应用于2个假设

问如何将引理应用于2个假设
EN

Stack Overflow用户

提问于 2020-07-29 04:13:25

回答 1查看 35关注 0票数 1

Theorem ev_plus_plus : forall n m p,
  even (n+m) -> even (n+p) -> even (m+p).
Proof.
  intros n m p Hnm Hnp.

我们得到这样的结果：

1 subgoal (ID 189)
  
  n, m, p : nat
  Hnm : even (n + m)
  Hnp : even (n + p)
  ============================
  even (m + p)

我们还有一个先前证明过的定理：

ev_sum
     : forall n m : nat, even n -> even m -> even (n + m)

我们知道(n+m)是偶数，(n+p)是偶数。如何在上下文中通过将ev_sum应用于Hnm和Hnp来创建新的假设：

Hsum: even((n+m) + (n+p))

回答已采纳

发布于 2020-07-29 04:20:15

为此，您有几种选择。您可以像这样使用pose proof：

pose proof (ev_sum _ _ Hnm Hnp) as Hsum.

它会做你所期望的事情。它允许您给出一个术语并将其添加为假设。

另一种选择是使用eapply ... in。例如，您可以这样做

eapply ev_sum in Hnm.

然后你必须在其中一个子目标中给它Hnp。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/63142082

复制

相似问题

问如何将引理应用于2个假设EN