3

我正在尝试使用 Omega 在 Coq 中进行证明。我花了很多时间在这上面，但什么都没有。不得不说我是Coq新手，所以对这种语言不太适应，也没有太多经验。但我正在努力。

这是我必须证明的代码：

Require Import Arith Omega.

Fixpoint div2 (n : nat) :=
 match n with
   S (S p) => S (div2 p)
 | _ => 0
 end.

Fixpoint mod2 (n : nat) :=
 match n with
   S (S p) => mod2 p
 | x => x
 end.

为了证明这一点，我认为首先通过归纳证明这个引理会有所帮助：

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.

然后这个，使用 omega 和 div2_eq ：

Lemma div2_le : forall n, div2 n <= n.

但我没能走得更远。

有谁知道该怎么做？

4

1 回答 1

4

您可以轻松地从函数中得出归纳原则，div2如下mod2所示：

Functional Scheme div2_ind := Induction for div2 Sort Prop.
Functional Scheme mod2_ind := Induction for mod2 Sort Prop.

div2_ind并mod2_ind有或多或少的类型：

forall P1,
  P1 0 0 ->
  P1 1 0 ->
  (forall n1, P1 n1 (div2 n1) -> P1 (S (S n1)) (S (div2 n1))) ->
  forall n1, P1 n1 (div2 n1)

forall P1,
  P1 0 0 ->
  P1 1 1 ->
  (forall n1, P1 n1 (mod2 n1) -> P1 (S (S n1)) (mod2 n1)) ->
  forall n1, P1 n1 (mod2 n1)

要应用这些定理，您可以方便地编写functional induction (div2 n)或functional induction (mod2 n)通常编写的地方induction n。

但更强的归纳原理与这些功能相关：

Lemma nat_ind_alt : forall P1 : nat -> Prop,
  P1 0 ->
  P1 1 ->
  (forall n1, P1 n1 -> P1 (S (S n1))) ->
  forall n1, P1 n1.
Proof.
intros P1 H1 H2 H3. induction n1 as [[| [| n1]] H4] using lt_wf_ind.
  info_auto.
  info_auto.
  info_auto.
Qed.

事实上，任何函数的域都是一个有用的归纳原理的线索。例如，与功能域相关的归纳原理plus : nat -> nat -> nat就是mult : nat -> nat -> nat结构归纳。这让我想知道为什么Functional Scheme不只是产生这些更一般的原则。

在任何情况下，您的定理证明将变为：

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl in *. omega.
  simpl in *. omega.
  simpl in *. omega.
Qed.

Lemma div2_le : forall n, div2 n <= n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl. omega.
  simpl. omega.
  simpl. omega.
Qed.

您应该熟悉功能归纳，但更重要的是，您应该真正熟悉有根据的归纳。

于 2012-12-15T21:38:30.277 回答