Induction hypothesis vs. termination checker

Using Coq
1

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?

2

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

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