如何证明奇数是COQ中NAT的双倍继承者? [英] How to prove a odd number is the successor of double of nat in coq?
本文介绍了如何证明奇数是COQ中NAT的双倍继承者?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我的奇数定义如下:
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
有人能帮我吗??T谢谢您
推荐答案
标准归纳允许您从n
跳到n+1
。下面是您的odd
函数
您需要从n
跳到n+2
。因此,我们需要的是一种更强有力的归纳。做到这一点的一种方法是证明:
Theorem question_1c:
forall n m, m <= n -> Odd m -> (oddb m = true).
通过n
的标准归纳(但对于所有m
较小)
这篇关于如何证明奇数是COQ中NAT的双倍继承者?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文