IndProp：ev_plus_plus

Question

(** **** 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.

为什么在表达式 even (n + m) 中找不到 "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)

这里发生了什么？

Answer 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.

您可以在 software-foundations https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html

中查看更多关于应用策略的信息

Answer 2

正在发生的事情是，Coq 统一了 H1 与 ev_ev__ev 的 even n 参数而不是 even (n+m)。

您可以准确地告诉 Coq 您希望 H1 去哪里，并使用 _ 通配符作为您让 Coq 计算细节的地方。

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

Check ev_ev__ev (n+m) m _ H1.

Answer 3

语句forall n m, even (n+m) -> even n -> even m.并不意味着"if we have that (n + m) is even then we have both that n is even and that m is even"（这是错误的，考虑n = m = 1）。相反，它意味着 "if we have that (n+m) is even, and we have that n is even, then we have that m is even".

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

IndProp：ev_plus_plus

IndProp: ev_plus_plus

coq

logical-foundations