代码之家 › 专栏 › 技术社区 › user4035

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

logical-foundations coq

1

user4035 · 技术社区 · 5 年前

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

1 回复 | 直到 5 年前

1

Théo Winterhalter Matthieu Sozeau 5 年前

你有几种选择。你可以用 pose proof

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

它会达到你期望的效果。它允许你给出一个术语,并把它作为一个假设。

eapply ... in . 例如,你能做到

eapply ev_sum in Hnm.

Hnp 在其中一个子目标中。