如何解决如何证明一个奇数是coq中nat的double的后继?
我的奇数定义如下:
Definition Odd n := exists k,n = 2*k+1.
我有一个奇数定义一个数字是否为奇数。
Fixpoint oddb (n : nat) { struct n } : bool :=
match n with
| 0 => false
| 1 => true
| S (S n) => oddb n
end.
我试图证明一个数字是否是 nat 的双精度数的后继;那么它是一个奇数。
Theorem question_1c:
forall n,Odd n -> (oddb n = true).
Proof.
unfold Odd. intros. inversion H.
rewrite H0. simpl. induction x.
- simpl. reflexivity.
- Admitted.
我坚持第二个目标..它表明我需要证明 Sx..我从现在开始的假设似乎没有帮助......
1 subgoal
n : nat
H : exists k : nat,n = 2 * k + 1
x : nat
H0 : n = 2 * S x + 1
IHx : n = 2 * x + 1 -> oddb (x + (x + 0) + 1) = true
______________________________________(1/1)
oddb (S x + (S x + 0) + 1) = true
谁能帮帮我??敲你
解决方法
标准归纳法让您从 n
跳到 n+1
。在这里使用您的 odd
函数
你需要从 n
跳转到 n+2
。所以需要的是更强的归纳。一种方法是证明:
Theorem question_1c:
forall n m,m <= n -> Odd m -> (oddb m = true).
通过对 n
的标准归纳(但对于所有 m
更小)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。