如何证明coq中的归纳步骤？答案

【问题标题】：How to prove the inductive step in coq?如何证明coq中的归纳步骤？
【发布时间】：2018-09-17 10:32:12
【问题描述】：

这里是Coq初学者，我最近一个人看完了“Logical Foundations”的前7章。

我正在尝试通过 Coq 中的归纳来创建证明 ∀ n>= 3, 2n+1 < 2^n.

我从destruct 开始删除错误假设，直到达到 n=3。然后，我对 n 进行归纳，n=3 的情况很简单，但是，如何证明归纳步骤？？

我可以看到目标成立。我可以使用destruct 进行案例分析来证明这一点，但无法以一般形式展示。

The functions I'm using are from "Logical Foundations" and can be seen here.

到目前为止我的证明：

(* n>=3, 2n+1 < 2^n *)
Theorem two_n_plus_one_leq_three_lt_wo_pow_n : forall n:nat,
    (blt_nat (two_n_plus_one n) (exp 2 n)) = true
       -> (bge_nat n 3) = true.   
Proof.
  intros n.
  destruct n.
  (* n = 0 *)
  compute.
  intros H.
  inversion H.

  destruct n.
  (* n = 1 *)
  compute.
  intros H.
  inversion H.  

  destruct n.
  (* n = 2 *)
  compute.
  intros H.
  inversion H.

  induction n as [ | k IHk].
  (* n = 3 *)
  - compute.
    reflexivity.
  - rewrite <- IHk.
    (* Inductive step... *)

【问题讨论】：

目前尚不清楚您要确切证明什么。证明n>= 3, 2n+1 < 2^n 没有任何意义。根据 Coq 代码，你想证明2n+1 < 2^n -> n >=3。不应该反过来吗？
只是觉得可能值得一提的是，如果您执行intros [|[|[|n]]]，您可以一步完成所有这些destruct n。然后根据你已经写的内容，intros [|[|[|n]]]; try (compute; intro H; inversion H). 应该能够创建并立即清除n=0,1,2 案例。

标签： coq induction

【解决方案1】：

好吧，因为这是家庭作业，我帮不了你很多。让我写下你在 math-comp 中提出的引理，它已经允许使用理智的符号：

Theorem two_n_plus_one_leq_three_lt_wo_pow_n n :
  2*n.+1 < 2^n -> 3 <= n.

【讨论】：

我尝试使用 Ssreflect 但由于我还不熟悉它，我决定用 manual 不太自然的符号重写。无论如何谢谢你@ejgallego

【解决方案2】：

缺少的重要部分是使归纳假设具有一般性。我能够使用generalize dependent k. 完成证明。

所以证明看起来像这样：

(* n ≥ 3, 2n + 1 < 2^n *)
Theorem two_n_plus_one_leq_three_lt_wo_pow_n : forall n:nat,
    (blt_nat (two_n_plus_one n) (exp 2 n)) = true
       -> (bge_nat n 3) = true.
Proof.
  intros n.
  destruct n.
  (* n = 0 *)
  compute.
  intros HF. (* Discard the cases where n is not >= 3 *)
  inversion HF.

  destruct n.
  (* n = 1 *)
  compute.
  intros HF.
  inversion HF.

  destruct n.
  (* n = 2 *)
  compute.
  intros HF.
  inversion HF.

  induction n as [ | k IHk].
  (* n = 3 *)
  - compute.
    reflexivity.
  (* n+1 inductive step *)
  - generalize dependent k.
    intros.
    compute.
    reflexivity.
Qed.

【讨论】：

您的解决方案中有两个大问题。首先，正如我在第一条评论中所述，您试图证明forall n, 2n+1 < 2^n -> n >= 3，但根据您的编辑，您真正想要证明的是forall n, n >= 3 -> 2n+1 < 2^n。其次，假设你真的想证明forall n, 2n+1 < 2^n -> n >= 3，那么你不需要归纳。您所要做的就是用n = 0, 1, 2 检验假设是矛盾的。在其他情况下，我们显然有n >= 3。
@eponier 感谢您的评论和查看证明。 1) 这是对于所有整数 n ≥ 3, 2n + 1 我认为这在 coq 中转换为 forall n, 2n+1 < 2^n -> n >= 3。 2) 本练习需要归纳，它来自 Susanna S. Epp 的“具有应用的离散数学”的命题 5.3.2
我不明白您是如何阅读 forall n, 2n+1 < 2^n -> n >= 3 的。像往常一样，这意味着：“forall n, if 2n+1 = 3”，而这不是你想要证明的。当然，对于最初的问题，您需要归纳，但对于这个问题则不需要。
@eponier 是正确的。如果您要证明英文陈述，对于所有整数 n >= 3, 2 n + 1 ，正确的 Coq 翻译是 forall n, n >= 3 -> 2*n+1 < 2^n。