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 (Yves)

There are many general patterns of induction like this one that can be covered by the existing library on well founded induction. In this case, you can prove any property P by induction on length of lists by using well_founded_induction, wf_inverse_image, and PeanoNat.Nat.lt_wf_0, as in the following command:

  induction l using (well_founded_induction
                       (wf_inverse_image _ nat _ (@length _)
                                         PeanoNat.Nat.lt_wf_0)).
T: Type
P: list T -> Prop
l: list T
H: forall y : list T, length y < length l -> P y
P l

if you are working with lists of type T and proving a goal P l, this generates an hypothesis of the form

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

This will apply to any other datatype (like trees for instance) as long as you can map that other datatype to nat using any size function from that datatype to nat instead of length.

Note that you need to add Require Import Wellfounded. at the head of your development for this to work.

A: Here is a slightly shorter variant:

  induction xs using (induction_ltof1 _ (@length _)); unfold ltof in *.
T: Type
P: list T -> Prop
xs: list T
H: forall y : list T, length y < length xs -> P y
P xs

But I'd prefer explicit naming:

  induction xs as [xs IHxs] using (induction_ltof1 _ (@length _));
    unfold ltof in IHxs.
T: Type
P: list T -> Prop
xs: list T
IHxs: forall y : list T, length y < length xs -> P y
P xs

Answer (James Wilcox)

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

Require Import List Lia.

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.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
forall xs : list A, P xs
  Proof.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
forall xs : list A, P xs
    assert (forall xs l : list A, length l <= length xs -> P l) as H_ind.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
forall xs l : list A, length l <= length xs -> P l
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
H_ind: forall xs l : list A,
length l <= length xs -> P l
forall xs : list A, P xs
    {
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
forall xs l : list A, length l <= length xs -> P l induction xs; intros l Hlen; apply H; intros l0 H0.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
l: list A
Hlen: length l <= length nil
l0: list A
H0: length l0 < length l
P l0
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
a: A
xs: list A
IHxs: forall l : list A, length l <= length xs -> P l
l: list A
Hlen: length l <= length (a :: xs)
l0: list A
H0: length l0 < length l
P l0
      -
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
l: list A
Hlen: length l <= length nil
l0: list A
H0: length l0 < length l
P l0 inversion Hlen.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
l: list A
Hlen: length l <= length nil
l0: list A
H0: length l0 < length l
H2: length l = 0
P l0 lia.
      -
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
a: A
xs: list A
IHxs: forall l : list A, length l <= length xs -> P l
l: list A
Hlen: length l <= length (a :: xs)
l0: list A
H0: length l0 < length l
P l0 apply IHxs.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
a: A
xs: list A
IHxs: forall l : list A, length l <= length xs -> P l
l: list A
Hlen: length l <= length (a :: xs)
l0: list A
H0: length l0 < length l
length l0 <= length xs simpl in Hlen.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
a: A
xs: list A
IHxs: forall l : list A, length l <= length xs -> P l
l: list A
Hlen: length l <= S (length xs)
l0: list A
H0: length l0 < length l
length l0 <= length xs lia.
    }
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
H_ind: forall xs l : list A,
length l <= length xs -> P l
forall xs : list A, P xs
    intros xs.
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
H_ind: forall xs l : list A,
length l <= length xs -> P l
xs: list A
P xs apply H_ind with (xs := xs).
A: Type
P: list A -> Prop
H: forall xs : list A,
(forall l : list A, length l < length xs -> P l) ->
P xs
H_ind: forall xs l : list A,
length l <= length xs -> P l
xs: list A
length xs <= length xs lia.
  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.

Require Import Coq.Init.Nat.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
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.
forall w : list input,
extend_delta A w = B <-> Nat.odd (one_num w) = true
Proof.
forall w : list input,
extend_delta A w = B <-> Nat.odd (one_num w) = true
  assert (forall w s, extend_delta s w = if Nat.odd (one_num w)
                                         then flip_state s
                                         else s).
forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
H: forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
forall w : list input,
extend_delta A w = B <-> Nat.odd (one_num w) = true
  {
forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s) induction w as [|i w]; intros s; simpl.
s: state
s = s
i: input
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
delta (extend_delta s w) i =
(if
  Nat.odd
    match i with
    | zero => one_num w
    | one => S (one_num w)
    end
 then flip_state s
 else s)
    -
s: state
s = s reflexivity.
    -
i: input
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
delta (extend_delta s w) i =
(if
  Nat.odd
    match i with
    | zero => one_num w
    | one => S (one_num w)
    end
 then flip_state s
 else s) rewrite IHw.
i: input
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
delta
  (if Nat.odd (one_num w) then flip_state s else s) i =
(if
  Nat.odd
    match i with
    | zero => one_num w
    | one => S (one_num w)
    end
 then flip_state s
 else s) destruct i; simpl.
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
(if Nat.odd (one_num w) then flip_state s else s) =
(if Nat.odd (one_num w) then flip_state s else s)
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
flip_state
  (if Nat.odd (one_num w) then flip_state s else s) =
(if Nat.odd (S (one_num w)) then flip_state s else s)
      +
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
(if Nat.odd (one_num w) then flip_state s else s) =
(if Nat.odd (one_num w) then flip_state s else s) reflexivity.
      +
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
flip_state
  (if Nat.odd (one_num w) then flip_state s else s) =
(if Nat.odd (S (one_num w)) then flip_state s else s) rewrite <- Nat.negb_even, Nat.odd_succ.
w: list input
IHw: forall s : state,
extend_delta s w = (if Nat.odd (one_num w) then flip_state s else s)
s: state
flip_state
  (if negb (Nat.even (one_num w))
   then flip_state s
   else s) =
(if Nat.even (one_num w) then flip_state s else s)
        destruct (Nat.even (one_num w)), s; reflexivity.
  }
H: forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
forall w : list input,
extend_delta A w = B <-> Nat.odd (one_num w) = true
  intros w.
H: forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
w: list input
extend_delta A w = B <-> Nat.odd (one_num w) = true rewrite H.
H: forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
w: list input
(if Nat.odd (one_num w) then flip_state A else A) = B <->
Nat.odd (one_num w) = true simpl.
H: forall (w : list input) (s : state),
extend_delta s w =
(if Nat.odd (one_num w) then flip_state s else s)
w: list input
(if Nat.odd (one_num w) then B else A) = B <->
Nat.odd (one_num w) = true
  destruct (Nat.odd (one_num w)); intuition congruence.
Qed.

Answer (ejgallego)

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

From mathcomp Require Import all_ssreflect.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

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.
T: Type
P: seq T -> Prop
s: seq T
P s
  Proof.
T: Type
P: seq T -> Prop
s: seq T
P s
    move: {2}(size _) (leqnn (size s)) => ss; elim: ss s => [|ss ihss] s hs.
T: Type
P: seq T -> Prop
s: seq T
hs: size s <= 0
P s
T: Type
P: seq T -> Prop
ss: nat
ihss: forall s, size s <= ss -> P s
s: seq T
hs: size s <= ss.+1
P s

End SO.

Just introduce a fresh nat for the size of the list, and regular induction will work.