The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

I have defined the head of a non-empty listn as follows.

  Implicit Arguments On.
  Section Listn.
  Variable A : Set.

  Inductive listn : nat->Set :=
    niln: (listn O) 
  | consn: (a:A)(n:nat)(listn n)->(listn (S n)).

  Definition hdn: (n:nat)(l:(listn (S n)))A.
  Intros n l. Inversion l. Exact a.
  Defined.

I was extremely impressed by the Inversion tactic that can handle this
definition (in LEGO we have to work much harder; see the development
of "vectors" in the LEGO library), but when I tried to use the
definition of "hdn" I found it doesn't compute as I expected

  Coq < Eval Compute in (hdn (consn O (niln nat))).
       = (<[n:nat]nat->(listn nat n)->nat>
            Cases
              (sym_eq nat O O
                (f_equal nat nat
                  [e:nat]Cases e of
                           O => O
                         | (S a) => a
                         end (S O) (S O) (refl_equal nat (S O))))
            of
              refl_equal => [a:nat; _:(listn nat O)]a
            end O (niln nat))
       : nat

I assume the cause is the Inversion tactic, but I don't understand
what's going on.  I'd appreciate both an explanation of what's
happening, and suggestions how to make such definitions as "hdn".

Randy