IndProp: ev_plus_plus
IndProp: ev_plus_plus
提问于 2019-05-25 20:16:34
(** **** 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但是它给出了两个子目标，我们需要证明的第二个目标比最初的一个要复杂得多：
even (n + m + m)这里发生了什么事？
Stack Overflow用户
回答已采纳
发布于 2019-05-26 17:49:33
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证明定理之前，我建议先弄清楚如何用笔和纸证明你的定理。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/56308378
复制相关文章
相似问题
腾讯云开发者
