# Induction hypothesis vs. termination checker

Hello!

I have the following slightly odd induction hypothesis for lists:

``````Definition list_induction_3 :
∀ (A : Type),
∀ (P : list A → Prop),
P [] →
(∀ (r : A), P (r :: [])) →
(∀ (r0 r1 : A) (rest : list A), P rest → P (r1 :: rest) → P (r0 :: r1 :: rest)) →
∀ (L : list A), P L :=
λ A
P
P_nil
P_1
P_more,
fix f (l : list A) :=
match l with
| []               => P_nil
| r :: []          => P_1 r
| r0 :: r1 :: rest => P_more r0 r1 rest (f rest) (f (r1 :: rest))
end.
``````

Essentially, It breaks induction into a case that handles `[]`, a case that handles `r :: []` and a case that handles `r0 :: r1 :: rest`. This doesn’t pass the termination checker with the following error:

``````A : Type
P : (list A) → Prop
P_nil : P []
P_1 : ∀ r : A, (P [r])
P_more : ∀ (r0 r1 : A) (rest : list A), ((P rest) → (P (r1 :: rest)) → P (r0 :: (r1 :: rest)))
f : ∀ l : list A, (P l)
l : list A
r0 : A
l0 : list A
r1 : A
rest : list A
Recursive call to f has principal argument equal to "r1 :: rest" instead of one of the following variables:
"l0" "rest".
Recursive definition is:
"λ l : list A,
match l as l0 return (P l0) with
| [] => P_nil
| r0 :: l0 =>
match l0 as l1 return (P (r0 :: l1)) with
| [] => P_1 r0
| r1 :: rest => P_more r0 r1 rest (f rest) (f (r1 :: rest))
end
end".
``````

I’m not 100% convinced that the function would terminate (that nested match is throwing me off a bit), but assuming that it does terminate, is there some other way I can write this to get Coq to accept it?

Here is a working version

``````Definition list_induction_3
(A : Type)
(P : list A -> Prop)
(H0: P [])
(H1: forall (r : A), P (r :: []))
(Hrec: forall (r0 r1 : A) (rest : list A),
P rest -> P (r1 :: rest) -> P (r0 :: r1 :: rest)):
forall (L : list A), P L :=
fix IHL (L : list A) : P L :=
match L with
| [] => H0
| r :: L0 =>
let IHL' := IHL L0 in
match L0 return (P L0 -> P (r :: L0)) with
| [] => fun _ => H1 r
| r1 :: rest =>
fun IHL' =>
Hrec r r1 rest (IHL rest) IHL'
end IHL'
end.
``````

The trick is to recurse on the first tail of the list before destructing it; otherwise Coq doesn’t realize that it’s a sublist of the input.

The hint is in this part of the error:

``````Recursive call to f has principal argument equal to "r1 :: rest" instead of one of the following variables:
"l0" "rest".
``````

Thank you! I don’t think I would have stumbled onto that one alone. I couldn’t work out how to tell Coq about the sublist.

If there’s one thing I think never gets particularly readable in Coq, it’s induction principles. 