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

Question

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?

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.

Answer 1

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.

You can use it like this

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.