如何在Coq列表的长度上进行归纳？

Question

当在纸上推理时,我经常通过归纳使用一些列表的长度.我想在Coq中形式化这些参数,但似乎没有任何内置的方法来对列表的长度进行归纳.

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

更具体地说,我试图证明这个定理.在纸面上,我通过归纳证明了它的长度w.我的目标是在Coq中形式化这个证明.

Answer 1

有许多一般的感应模式,如现有的图书馆,可以通过有根据的归纳法来涵盖.在这种情况下,可以通过诱导对名单的长度,通过使用证明任何属性P well_founded_induction,wf_inverse_image和PeanoNat.Nat.lt_wf_0,如下面的COMAND:

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

这将适用于任何其他数据类型(例如树),只要您可以将该其他数据类型映射到nat使用该数据类型中的任何大小函数nat而不是length.

请注意,您需要添加Require Import Wellfounded.开发的头部才能使其正常工作.

Answer 2

以下是如何证明一般列表长度归纳原理.

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.