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?