时间戳

首页 > 解决方案 > 如何证明一个奇数是coq中nat的double的后继？

coq - 如何证明一个奇数是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

谁能帮我？？谢谢你

标签： coq

解决方案

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

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

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

推荐阅读