如何对 Coq 中列表的长度进行归纳？

Question

在纸上推理时，我经常对一些列表的长度进行归纳论证。我想在 Coq 中将这些参数形式化，但似乎没有任何内置方法可以对列表的长度进行归纳。

我应该如何进行这样的归纳？

更具体地说，我试图证明this theorem。在纸上，我对w的长度进行了归纳证明。我的目标是在 Coq 中形式化这个证明。

Answer 1

这里是证明一般列表长度归纳原理的方法。

Require Import List Omega.

Section list_length_ind.  
  Variable A : Type.
  Variable P : list A -> Prop.

  Hypothesis H : forall xs, (forall l, length l < length xs -> P l) -> P xs.

  Theorem list_length_ind : forall xs, P xs.
  Proof.
    assert (forall xs l : list A, length l <= length xs -> P l) as H_ind.
    { induction xs; intros l Hlen; apply H; intros l0 H0.
      - inversion Hlen. omega.
      - apply IHxs. simpl in Hlen. omega.
    }
    intros xs.
    apply H_ind with (xs := xs).
    omega.
  Qed.
End list_length_ind.

你可以这样使用它

Theorem foo : forall l : list nat, ...
Proof. 
    induction l using list_length_ind.
    ...

也就是说，您的具体示例不一定需要对长度进行归纳。你只需要一个足够普遍的归纳假设。

Import ListNotations.

(* ... some definitions elided here ... *)    

Definition flip_state (s : state) :=
  match s with
  | A => B
  | B => A
  end.

Definition delta (s : state) (n : input) : state :=
  match n with
  | zero => s
  | one => flip_state s
  end.

(* ...some more definitions elided here ...*)

Theorem automata221: forall (w : list input),
    extend_delta A w = B <-> Nat.odd (one_num w) = true.
Proof.
  assert (forall w s, extend_delta s w = if Nat.odd (one_num w) then flip_state s else s).
  { induction w as [|i w]; intros s; simpl.
    - reflexivity.
    - rewrite IHw.
      destruct i; simpl.
      + reflexivity.
      + rewrite <- Nat.negb_even, Nat.odd_succ.
        destruct (Nat.even (one_num w)), s; reflexivity.
  }

  intros w.
  rewrite H; simpl.
  destruct (Nat.odd (one_num w)); intuition congruence.
Qed.

Answer 2

有许多像这样的通用归纳模式可以涵盖由现有图书馆对有根据的归纳。在这种情况下，你可以证明任何属性 P 通过使用 well_founded_induction、wf_inverse_image 和 PeanoNat.Nat.lt_wf_0 对列表长度进行归纳，如以下命令：

induction l using (well_founded_induction
                     (wf_inverse_image _ nat _ (@length _)
                        PeanoNat.Nat.lt_wf_0)).

如果您正在使用 T 类型的列表并证明目标 P l，这会生成一个形式的假设

H : forall y : list T, length y < length l -> P y

这将适用于任何其他数据类型（例如树），只要您可以使用来自该数据类型的任何 size 函数将该其他数据类型映射到 nat nat 而不是 length.

请注意，您需要在开发的开头添加 Require Import Wellfounded. 才能正常工作。

Answer 3

在这种情况下，直接概括引理通常会更快：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section SO.

Variable T : Type.
Implicit Types (s : seq T) (P : seq T -> Prop).

Lemma test P s : P s.
Proof.
move: {2}(size _) (leqnn (size s)) => ss; elim: ss s => [|ss ihss] s hs.

只需为列表的大小引入一个新的nat，常规归纳就可以了。

如何对 Coq 中列表的长度进行归纳？

How to do induction on the length of a list in Coq?

coq

induction