coq - 如何将引理应用于 2 个假设

Question

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))

?

Answer 1

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

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

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

另一种选择是使用eapply ... in. 例如你可以做

eapply ev_sum in Hnm.

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