如何证明一个奇数是coq中nat的double的后继？答案

【问题标题】：How to prove a odd number is the successor of double of nat in coq?如何证明一个奇数是coq中nat的double的后继？
【发布时间】：2023-03-11 02:06:01
【问题描述】：

我的奇数定义如下：

Definition Odd n := exists k, n = 2*k+1.

而且我有一个oddb 来定义一个数字是否为奇数。

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

谁能帮帮我？？谢谢你

【问题讨论】：

标签： coq

【解决方案1】：

标准归纳让您从n 跳转到n+1。这里有你的odd 功能您需要从n 跳转到n+2。所以需要的是更强的感应。一种方法是证明：

Theorem question_1c:
  forall n m, m <= n -> Odd m -> (oddb m = true).

通过n 的标准归纳（但对于所有m 更小）

【讨论】：