由网友(Take love)分享简介：我的奇数定义如下：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...

我的奇数定义如下：

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较小)