Define list length in recursion in Coq Not sure if my function is wrong and got stuck

So i was trying to define a tail-recursive version of list length function and prove that the function is the same as "length" function Below is my code. Got stuck when prove

Fixpoint length_tail (A: Type) (l: list A) (len: nat): nat :=
  match l, len with
  | [], len => len
  | _ :: t, len => length_tail _ t (1 + len)
end.

Example length_rev: forall {A: Type} {l1: list A}, 
  @length_tail _ l1 0 = @length _ l1.
Proof.
  intros.
  induction l1.
  - simpl. reflexivity.
  - simpl.
    rewrite <- IHl1.
    + simpl.
Admitted.

Below is the original function for the "length":

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O
  | h :: t => S (length t)
  end.

Tons of appreciations if anyone could help or give some hints!! Thanks!

Solution

Several things:

First, you pattern-match on both l and len the accumulator in your function but you are not looking at its shape, the following would do just as well:

Fixpoint length_tail (A: Type) (l: list A) (len: nat): nat :=
  match l with
  | [] => len
  | _ :: t => length_tail _ t (1 + len)
  end.

Second, the problem you are facing is that the lemma you want to prove by induction is not general enough. Indeed you are assuming that the accumulator is 0, but as you can see in the recursive call, you have 1 + len (which is just S len by the way), which will never be equal to 0.

In order to prove this by induction you need to prove something stronger. Typically you want to give an expression that is equal to length_tail l len in terms of length l such that when instantiated with 0 you get length l.

To me it sounds like length_tail l len = len + length l is a good candidate. You will have to do this often when proving properties about functions with accumulators.

There are several ways to go about this:

You could directly prove the more general lemma and then have a corollary, it could be useful for other things.
You can use assert of the stronger lemma in your proof and then conclude with it.
Or you can generalize your goal in your proof. I would personally not use it but I will show it to illustrate what one can do.

Fixpoint length_tail {A : Type} (l: list A) (len: nat): nat :=
  match l, len with
  | [], len => len
  | _ :: t, len => length_tail t (1 + len)
end.

Example length_rev : forall {A: Type} {l : list A},
  length_tail l 0 = length l.
Proof.
  intros A l.
  change (length l) with (0 + length l).
  generalize 0 as n.
  (* Now the goal is forall n : nat, length_tail l n = n + length l *)

Note that I marked the type as implicit in length_tail, this way it's much more readable don't you think?