在 Coq 中获得更强的归纳原理

Question

假设如下：

Inductive bin : Set := Z | O.

Fixpoint fib (n : nat) : list bin :=
  match n with
    | 0   => [Z]
    | S k => match k with
               | 0    => [O]
               | S k' => fib k' ++ fib k
             end
  end.

我想展示：

Theorem fib_first : forall n,
    Nat.Even n -> n > 3 -> exists w, fib n = Z :: w.

但是，通过在 n 上执行 induction，我得到了一个非常无用的归纳修正假设 n，说明 IH : Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w。

我最理想的是：IH : forall n : nat, Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w。当然我不能假设原来的命题，但我觉得我可能需要证明一些更强大的东西？

我的归纳推理的想法可以通过扩展 F n = F n-2 . F n-1 来实现，我们知道 F n-2 是偶数当且仅当 F n 是偶数，并且因为 F n-2或 F n-1 为空，我们可以证明子串更短，因此足以满足归纳假设——如何在 Coq 中表达这一点？

Answer 1

诀窍是展开 Nat.Even 的定义并对 n / 2 而不是 n 进行归纳：

Theorem fib_first : forall n,
  Nat.Even n -> exists w, fib n = Z :: w.
Proof.
intros n [m ->].
induction m as [|m IH].
- now exists nil.
- rewrite <- mult_n_Sm, plus_comm.
  generalize (2 * m) IH. clear m IH. simpl.
  intros n [w ->].
  simpl. eauto.
Qed.

请注意，您的 n > 3 假设实际上并不需要。

在 Coq 中获得更强的归纳原理

Getting a stronger induction principle in Coq

coq

theorem-proving