I want to prove some properties about list, but am stuck at induction

I tried following proof,

Require Import List Omega.
Import ListNotations.
Variable X : Type.

Lemma length_n_nth_app_error_same : forall (n:nat) (x:X) (l:list X),
n <= length l -> 0 < n -> nth_error l n = nth_error (l ++ [x]) n .
Proof.
  intros.
  induction l eqn:eqHl.
  - unfold length in H. omega.
  -

but I'm stuck, as what I have is only

1 subgoal
n : nat
x : X
l : list X
a : X
l0 : list X
eqHl : l = a :: l0
H : n <= length (a :: l0)
H0 : 0 < n
IHl0 : l = l0 ->
       n <= length l0 ->
       nth_error l0 n = nth_error (l0 ++ [x]) n
______________________________________(1/1)
nth_error (a :: l0) n = nth_error ((a :: l0) ++ [x]) n

I've met some similar cases also for other proofs on lists. I don't know if the usual induction would be useful here.

How should I prove this? Should I use generalize?

Solution

Your theorem is wrong. Maybe your understanding of nth_error is incorrect.

Specifically, when n = length l, nth_error l n returns None while nth_error (l ++ [x]) n returns Some x.

Require Import List Omega.
Import ListNotations.

Lemma length_n_nth_app_error_not_always_same :
  (forall (n:nat) (X:Type) (x:X) (l:list X),
  n <= length l -> 0 < n -> nth_error l n = nth_error (l ++ [x]) n)
  -> False.
Proof.
  intros.
  assert (1 <= 1) by omega. assert (0 < 1) by omega.
  specialize (H 1 nat 2 [1] H0 H1). simpl in H. inversion H. Qed.

On the other hand, proving a similar theorem with fixed inequality is easy:

Lemma length_n_nth_app_error_same : forall (n:nat) (X:Type) (x:X) (l:list X),
n < length l -> nth_error l n = nth_error (l ++ [x]) n .
Proof.
  induction n; intros.
  - simpl. destruct l; simpl in *.
    + omega.
    + reflexivity.
  - simpl. destruct l; simpl in *.
    + omega.
    + apply IHn. omega. Qed.

Note that I used induction n instead of induction l. It is mainly because nth_error does recursive calls on decreasing n.

Also, if you felt like an induction hypothesis is not general enough, it is probably because your order of intros and induction was wrong. The rule of thumb is to start the proof by induction, and then intros the variables. If it is still not enough, you can revert dependent all the variables other than the one to do induction, and then induction x; intros.