0 
(** **** Exercise: 3 stars, standard, optional (ev_plus_plus)

    This exercise just requires applying existing lemmas.  No
    induction or even case analysis is needed, though some of the
    rewriting may be tedious. *)

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

这是我得到的：

1 subgoal (ID 89)

n, m, p : nat
H1 : even (n + m)
H2 : even (n + p)
============================
even (m + p)

我已经证明了前面的定理：

Theorem ev_ev__ev : forall n m,
  even (n+m) -> even n -> even m.

并想将其应用于 H1，但是

apply ev_ev__ev in H1.

给出一个错误：

Error: Unable to find an instance for the variable m.

为什么在表达式中找不到“m” even (n + m)？怎么修？

更新

apply ev_ev__ev with (m:=m) in H1.

给出了一个非常奇怪的结果：

2 subgoals (ID 90)

n, m, p : nat
H1 : even m
H2 : even (n + p)
============================
even (m + p)

subgoal 2 (ID 92) is:
 even (n + m + m)

我认为它会将 H1 转换为 2 假设：

H11 : even n
H12 : even m

但相反，它给出了 2 个子目标，我们需要证明的第二个子目标比最初的更复杂：

even (n + m + m)

这里发生了什么事？

4

3 回答 3

2

该陈述forall n m, even (n+m) -> even n -> even m.并不意味着“如果我们有 (n + m) 是偶数，那么我们同时拥有 n 是偶数和 m 是偶数”（这是错误的，考虑 n = m = 1）。相反，它的意思是“如果我们有 (n+m) 是偶数，并且我们有那个 n 是偶数，那么我们有那个 m 是偶数”。

如果不假设矛盾，就没有办法得到H11 : even n和H12 : even m只是从。H1 : even (n + m)我建议先弄清楚如何用笔和纸证明你的定理，然后再尝试在 Coq 中证明它。

于 2019-05-26T17:49:33.047 回答
1

因为 Coq 无法确定它应该为 m 赋予什么值。您可以应用该策略 eapply ev_ev__ev in H1.并查看目标

  n, m, p : nat
  H2 : even (n + p)
  H1 : even ?m
  ============================
  even (m + p)

subgoal 2 (ID 17) is:
 even (n + m + ?m)

Coq 已经用元变量 ?m 实例化了 m，最后你需要为这个元变量提供见证以完成证明。

第二种方法只是应用实例化 m 值的策略apply ev_ev__ev with (m := m) in H1.

您可以在软件基金会https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html中看到更多关于应用策略的信息

于 2019-05-26T01:14:15.687 回答
1

正在发生的事情是 CoqH1与even n参数 ofev_ev__ev而不是even (n+m).

你可以准确地告诉 Coq 你想去哪里，并在你让 Coq 计算细节的地方H1使用通配符。_

你可能想要这个ev_ev__ev n m H1带有类型的术语，even n -> even m但是你apply产生了这个术语ev_ev__ev (n+m) m _ H1 ，这也给你留下了更多需要证明的东西。要查看证明上下文，请执行

Check ev_ev__ev (n+m) m _ H1.
于 2019-05-26T09:28:12.683 回答