how to prove 2 step induction of list in coq using fix tactic

I want to prove 2 step induction for list by using fix tactic

In the following attempt to prove it I made goal structurally smaller(by applying pxy to the goal) before calling self, so I expect that calling self inside same theorem should not cause infinite recursion.

From Coq Require Import Lists.List.
Import ListNotations.

Lemma list_back_inversion : forall {X : Type} (l : list X), 
  l = [] \/ exists y l', l = l' ++ [y].
  induction l.
  - auto.
  - right. destruct IHl; subst.
    + exists a. exists []. reflexivity.
    + destruct H. destruct H. subst. exists x. exists (a::x0). reflexivity.
Qed. 

Theorem list_2_step_ind: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> forall l' : list X, P l'.
Proof.
  fix self 6.
  intros X P p0 px pxy l.
  destruct l.
  - apply p0.
  - destruct (list_back_inversion l).
    + subst. apply px.
    + destruct H. destruct H. subst. apply pxy. apply (self _ _ p0 px pxy).
Qed.

But I am getting this error

Recursive definition of self is ill-formed.
In environment
...

Recursive call to self has principal argument equal to 
"x3" instead of one of the following variables: "l0"

I know how to prove this theorem by using other tactics, but now I want to prove theorem by using fix to learn more about it

Solution

As mentioned in the comments, coq throws that error because termination checker not able to prove that l is structurally smaller than l ++ [y]. it is possible to add new argument which will be equal to length of list and use fix tactic against it.

From Coq Require Import Lists.List.
Import ListNotations.
Require Import Lia.

Lemma list_back_inversion : forall {X : Type} (l : list X), 
  l = [] \/ exists y l', l = l' ++ [y].
  induction l.
  - auto.
  - right. destruct IHl; subst.
    + exists a. exists []. reflexivity.
    + destruct H. destruct H. subst. exists x. exists (a::x0). reflexivity.
Qed. 


Theorem list_2_step_with_length_arg: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> 
  (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> 
  forall (l : list X) (len : nat) {L: len = length l}, P l.
Proof.
  fix self 7.
  intros X P p0 px pxy l len leq.

  (* to pass requirements of termination checker we need to 
  destruct len first to end this function when len reach to 0 *)

  destruct len; destruct l; simpl in *. 
  - apply p0.
  - inversion leq.
  - inversion leq.
  - destruct (list_back_inversion l).
      * subst. apply px.
      * destruct H. destruct H. subst. apply pxy. 
      apply (self _ _ p0 px pxy x1 (len - 1)).
      simpl in *. inversion leq. rewrite app_length. simpl. lia. 
Qed.

Theorem list_2_step: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> forall (l : list X), P l.
Proof.
  intros X P p0 px pxy l.
  apply (@list_2_step_with_length_arg X P p0 px pxy l (length l) eq_refl).
Qed.