How to do induction differently?

Question

I am doing an exercise in Coq and trying to prove if a list equals to its reverse, it's a palindrome. Here is how I define palindromes:

Inductive pal {X : Type} : list X -> Prop :=
| emptypal : pal []
| singlpal : forall x, pal [x]
| inducpal : forall x l, pal l -> pal (x :: l ++ [x]).

Here is the theorem:

Theorem palindrome3 : forall {X : Type} (l : list X),
    l = rev l -> pal l.
forall (X : Type) (l : list X), l = rev l -> pal l

According to my definition, I will need to do the induction my extracting the front and tail element but apparently coq won't let me do it, and if I force it to do so, it gives an induction result that definitely doesn't make any sense:

Proof.
forall (X : Type) (l : list X), l = rev l -> pal l
  intros X l H.
X: Type
l: list X
H: l = rev l
pal l remember (rev l) as rl.
X: Type
l, rl: list X
Heqrl: rl = rev l
H: l = rl
pal l induction l, rl.
X: Type
Heqrl: [] = rev []
H: [] = []
pal []
X: Type
x: X
rl: list X
Heqrl: x :: rl = rev []
H: [] = x :: rl
pal []
X: Type
a: X
l: list X
Heqrl: [] = rev (a :: l)
H: a :: l = []
IHl: [] = rev l -> l = [] -> pal l
pal (a :: l)
X: Type
a: X
l: list X
x: X
rl: list X
Heqrl: x :: rl = rev (a :: l)
H: a :: l = x :: rl
IHl: x :: rl = rev l -> l = x :: rl -> pal l
pal (a :: l)
  -
X: Type
Heqrl: [] = rev []
H: [] = []
pal [] apply emptypal.
  -
X: Type
x: X
rl: list X
Heqrl: x :: rl = rev []
H: [] = x :: rl
pal [] inversion H.
  -
X: Type
a: X
l: list X
Heqrl: [] = rev (a :: l)
H: a :: l = []
IHl: [] = rev l -> l = [] -> pal l
pal (a :: l) inversion H.
  - (* stuck *)
X: Type
a: X
l: list X
x: X
rl: list X
Heqrl: x :: rl = rev (a :: l)
H: a :: l = x :: rl
IHl: x :: rl = rev l -> l = x :: rl -> pal l
pal (a :: l)

context:

1 subgoal

  X : Type
  a : X
  l : list X
  x : X
  rl : list X
  Heqrl : x :: rl = rev (a :: l)
  H : a :: l = x :: rl
  IHl : x :: rl = rev l -> l = x :: rl -> pal l
  ============================
  pal (a :: l)

apparently the inductive context is terribly wrong. is there any way I can fix the induction?

Answer

The solution I propose here is probably not the shortest one, but I think it is rather natural.

My solution consists in defining an induction principle on list specialized to your problem.

Consider natural numbers. There is not only the standard induction nat_ind where you prove P 0 and forall n, P n -> P (S n). But there are other induction schemes, e.g., the strong induction lt_wf_ind, or the two-step induction where you prove P 0, P 1 and forall n, P n -> P (S (S n)). If the standard induction scheme is not strong enough to prove the property you want, you can try another one.

We can do the same for lists. If the standard induction scheme list_ind is not enough, we can write another one that works. In this idea, we define for lists an induction principle similar to the two-step induction on nat (and we will prove the validity of this induction scheme using the two-step induction on nat), where we need to prove three cases: P [], forall x, P [x] and forall x l x', P l -> P (x :: l ++ [x']). The proof of this scheme is the difficult part. Applying it to deduce your theorem is quite straightforward.

I don't know if the two-step induction scheme is part of the standard library, so I introduce it as an axiom.

Axiom nat_ind2 : forall P : nat -> Prop,
    P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.

Then we prove the induction scheme we want.

Lemma list_ind2 :
  forall {A} (P : list A -> Prop)
         (P_nil : P [])
         (P_single : forall x, P [x])
         (P_cons_snoc : forall x l x', P l -> P (x :: l ++ [x'])),
  forall l, P l.
forall (A : Type) (P : list A -> Prop),
P [] ->
(forall x : A, P [x]) ->
(forall (x : A) (l : list A) (x' : A),
 P l -> P (x :: l ++ [x'])) -> forall l : list A, P l
Proof.
forall (A : Type) (P : list A -> Prop),
P [] ->
(forall x : A, P [x]) ->
(forall (x : A) (l : list A) (x' : A),
 P l -> P (x :: l ++ [x'])) -> forall l : list A, P l
  intros.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
P l remember (length l) as n.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
n: nat
Heqn: n = length l
P l symmetry in Heqn.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
n: nat
Heqn: length l = n
P l revert dependent l.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
forall l : list A, length l = n -> P l
  induction n using nat_ind2; intros.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
Heqn: length l = 0
P l
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
Heqn: length l = 1
P l
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
l: list A
Heqn: length l = S (S n)
P l
  -
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
Heqn: length l = 0
P l apply length_zero_iff_nil in Heqn.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
Heqn: l = []
P l subst l.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
P [] apply P_nil.
  -
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
l: list A
Heqn: length l = 1
P l destruct l; [discriminate|].
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
a: A
l: list A
Heqn: length (a :: l) = 1
P (a :: l) simpl in Heqn.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
a: A
l: list A
Heqn: S (length l) = 1
P (a :: l) inversion Heqn; subst.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
a: A
l: list A
Heqn: S (length l) = 1
H0: length l = 0
P (a :: l)
    apply length_zero_iff_nil in H0.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
a: A
l: list A
Heqn: S (length l) = 1
H0: l = []
P (a :: l) subst l.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
a: A
Heqn: S (length []) = 1
P [a] apply P_single.
  -
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
l: list A
Heqn: length l = S (S n)
P l destruct l; [discriminate|].
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: length (a :: l) = S (S n)
P (a :: l) simpl in Heqn.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
P (a :: l)
    inversion Heqn; subst.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
P (a :: l) pose proof (rev_involutive l) as Hinv.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
Hinv: rev (rev l) = l
P (a :: l)
    destruct (rev l).
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
Hinv: rev [] = l
P (a :: l)
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
a0: A
l0: list A
Hinv: rev (a0 :: l0) = l
P (a :: l) destruct l; discriminate.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
a0: A
l0: list A
Hinv: rev (a0 :: l0) = l
P (a :: l) simpl in Hinv.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a: A
l: list A
Heqn: S (length l) = S (S n)
H0: length l = S n
a0: A
l0: list A
Hinv: rev l0 ++ [a0] = l
P (a :: l) subst l.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: length (rev l0 ++ [a0]) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
P (a :: rev l0 ++ [a0])
    rewrite app_length in H0.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: length (rev l0) + length [a0] = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
P (a :: rev l0 ++ [a0])
    rewrite PeanoNat.Nat.add_comm in H0.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: length [a0] + length (rev l0) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
P (a :: rev l0 ++ [a0]) simpl in H0.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: S (length (rev l0)) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
P (a :: rev l0 ++ [a0]) inversion H0.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: S (length (rev l0)) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
H1: length (rev l0) = n
P (a :: rev l0 ++ [a0])
    apply P_cons_snoc.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: S (length (rev l0)) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
H1: length (rev l0) = n
P (rev l0) apply IHn.
A: Type
P: list A -> Prop
P_nil: P []
P_single: forall x : A, P [x]
P_cons_snoc: forall (x : A) (l : list A) (x' : A),
P l -> P (x :: l ++ [x'])
n: nat
IHn: forall l : list A, length l = n -> P l
a, a0: A
l0: list A
H0: S (length (rev l0)) = S n
Heqn: S (length (rev l0 ++ [a0])) = S (S n)
H1: length (rev l0) = n
length (rev l0) = n assumption.
Qed.

You should be able to conclude quite easily using this induction principle.

Theorem palindrome3 : forall {X : Type} (l : list X),
    l = rev l -> pal l.
forall (X : Type) (l : list X), l = rev l -> pal l

A: Yes, there is that induction principle in the standard library, see pair_induction.