A simple Coq proof exercise.

ManualInversion.v

(* Consider lists indexed by length. *)

Inductive List (t : Type) : nat -> Type :=
  | Nil : List t 0
  | Cons : forall n, t -> List t n -> List t (S n).

(* Every non-empty list has a head element. *)

Definition Head : forall t n, List t (S n) -> t.
intros t n list. inversion list. assumption. Defined.

(* In the proof, "inversion" tactic saved the day, eliminating the
"Nil" case. However, the body of the proof term is not very
pretty. Consider: *)

Print Head.

(* 

Head = 
fun (t : Type) (n : nat) (list : List t (S n)) =>
let X :=
  match list in (List _ n0) return (n0 = S n -> t) with
  | Nil =>
      fun H : 0 = S n =>
      let H0 :=
        eq_ind 0 (fun e : nat => match e with
                                 | 0 => True
                                 | S _ => False
                                 end) I (S n) H in
      False_rect t H0
  | Cons n0 X X0 =>
      fun H : S n0 = S n =>
      let H0 :=
        let H0 :=
          f_equal (fun e : nat => match e with
                                  | 0 => n0
                                  | S n1 => n1
                                  end) H in
        eq_rect n (fun n1 : nat => t -> List t n1 -> t)
          (fun (X1 : t) (_ : List t n) => X1) n0 (eq_sym H0) in
      H0 X X0
  end in
X (eq_refl (S n))
     : forall (t : Type) (n : nat), List t (S n) -> t

*)

(* Whoah, what a proof! Can we do better manually? Yes, if we find a
way to discharge the "Nil" case. Dependent pattern-matching to the
rescue: *)

Definition HeadManual t n (list: List t (S n)) : t :=
  match list in List _ k return match k with
                                  | O => unit
                                  | S _ => t 
                                end with
    | Nil => tt
    | Cons _ x _ => x
  end.

(* This worked out because "O" case never matches, that is, we
exploited the contradiction and were allowed to return unit.  The
automated proof was more explicit about it, deriving an arbitrary
value from "0 = S n" which implies "False".  This example is very
simple and in a sense we were lucky here.  For more involved worked
examples see this CPDT chapter:
http://adam.chlipala.net/cpdt/html/DataStruct.html *)