如何在Coq中对列表长度进行归纳？ [英] How to do induction on the length of a list in Coq?

问题描述

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

When reasoning on paper, I often use arguments by induction on the length of some list. I want to formalized these arguments in Coq, but there doesn't seem to be any built in way to do induction on the length of a list.

我应该如何进行这种归纳？

How should I perform such an induction?

更具体地说，我正在尝试证明这个定理。在纸上，我通过归纳证明了 w 的长度。我的目标是将此证明正式化为Coq。

More concretely, I am trying to prove this theorem. On paper, I proved it by induction on the length of w. My goal is to formalize this proof in Coq.

推荐答案

在这里是如何证明一般的列表长度归纳原理。

Here is how to prove a general list-length induction principle.

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.
    ...

---

您的具体示例示例不一定需要对长度进行归纳。您只需要一个足够笼统的归纳假设。

---

That said, your concrete example example does not necessarily need induction on the length. You just need a sufficiently general induction hypothesis.

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.

这篇关于如何在Coq中对列表长度进行归纳？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！