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

Question

When reasoning on paper, I often use arguments by induction over the length of a list. I want to formalize these arguments in Coq, but there seems to be no built-in way to induce the length of the list.

How can I do such an induction?

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

Answer 1

Here's how to prove the general principle of inducing list length.

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

---

, . .

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

(, ), nat nat length.

, Require Import Wellfounded. .

Answer 3

In this case, it is often faster to generalize your lemma directly:

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.

Just enter a new one natfor the list size and regular induction will work.