Proving some theorems on the function index in Coq

Question

I’m trying to implement an index function in Coq. I’ve written this code:

Notation grid := (list nat).

Fixpoint index_aux (n : nat) (g : grid) (i : nat) : option nat :=
  match g with
  | [] => None
  | h :: t => if h =? n then Some i else index_aux n t (i + 1)
  end.

Definition index (n : nat) (g : grid) : option nat :=
  index_aux n g 0.

And I tried to prove some theorems about it. First, some simple lemmas:

Lemma index_nil : forall x, index x [] = None.
Proof. auto. Qed.

Lemma index_singleton : forall x, index x [x] = Some 0.
Proof.
  intros x. unfold index. simpl. destruct (x =? x) eqn:E.
  reflexivity. rewrite Nat.eqb_neq in E. contradiction.
Qed.

Lemma index_double : forall x, index x [x; x] = Some 0.
Proof.
  intros x. unfold index. simpl. destruct (x =? x) eqn:E.
  reflexivity. rewrite Nat.eqb_neq in E. contradiction.
Qed.

And now, I’m trying to prove a more general theorem:

Theorem index_in : forall l x, In x l -> exists n, index x l = Some n.
Proof.
  intros l x H. induction l.
  - destruct H.
  - destruct H as [-> | H].
    + exists 0. unfold index. simpl. destruct (x =? x) eqn:E.
      * reflexivity.
      * rewrite Nat.eqb_neq in E. contradiction.
    + apply IHl in H as [n Hn].
      unfold index. simpl. destruct (a =? x) eqn:E.
      * exists 0. reflexivity.
      *

I’ve two questions:

1. In the lemmas I’ve proved, are there better proofs? Or using destruct and Nat.eqb_neq is a good way to prove it?
2. I’ve no clues about what would be the following tactics to prove the theorem. I don’t know how to infer the existence of n from In x l. How can I do? (I’ll accept clues instead of a full answer. I still want to prove it on my own, but I’m stuck.)

Edit: Thanks to Pierre Courtieu’s answer, I proved my theorem. In case it would help someone, here is what I did:

Theorem index_in : forall l x, In x l -> exists n, index x l = Some n.
Proof.
  unfold index. intro l. generalize dependent 0. induction l.
  - intros _ _ [].
  - intros n x H. unfold index_aux. destruct (a =? x) eqn:E; fold index_aux.
    + exists n. reflexivity.
    + rewrite Nat.eqb_neq in E. destruct H as [->|H].
      * contradiction.
      * apply IHl with (n:=n + 1) in H. assumption.
Qed.

Answer 1

2 clues:

1. proving directly the property on index means you prove a property about forall x l, index_aux x l 0 which is probably not general enough (you will end up needing something about index_aux x l <something else>). This is a general rule (even for pen and paper proofs): a proof by induction may need to be generalized for the induction to actually work. Edit: after trying it myself it turns out you do need something about the third argument of index_aux but you don't need to necessarily generalize your goal.
2. Be careful not to use the induction hypothesis too early.

Edit 3.And be also careful when you start your induction: try intro l. induction l. instead of intros l x H. induction l and compare induction hypothesis. You will see that x and H are quantified in the former case.