题
我陷入了“作为练习而留下”的引理 本次讲座. 。事情是这样的:
Lemma even_double : forall n, even n -> exists k, n = 2 * k.
Proof.
intros n H.
induction H.
...
在哪里 even
是一个归纳谓词,定义如下:
Inductive even : nat -> Prop :=
| even0 : even 0
| evenS : forall p:nat, even p -> even (S (S p).
请帮助?我总是以 (S (S p) = 2
或类似的。
编辑
我使用的一些引理和策略(不完整的证明):
destruct IHeven
exists (S x)
rewrite mult_succ_l
apply eq_S
apply plus_n_Sm
解决方案
归纳步骤之后,您应该有两个目标。
第一个(基本情况 even0
)应该很容易证明。存在证人应该被选为 0
, ,之后目标应该通过反身性保持。
第二种情况(对于 evenS
)看起来像:
p : nat
H : even p
IHeven : exists k : nat, p = 2 * k
============================
exists k : nat, S (S p) = 2 * k
IHeven
说存在一个数字(让我们命名它 k1
)这样 p = 2 * k1
.
你的目标是展示一些数字(比如, k2
)这样你就可以证明 S (S p) = 2 * k2
.
如果你计算一下,你应该会看到 (S k1)
将是完美的候选人。
因此,要继续,您可以使用以下策略:
destruct
破坏IHeven
分离证人k1
并证明p = 2 * k1
.exists
展出(S k1)
作为你目标的存在见证人。- 然后做一些工作来证明等式成立。
不隶属于 StackOverflow