如何将引理应用于 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。

How to apply a lemma to 2 hypothesis