The Coq mailing list

[cornes AT fing.edu.uy (Cristina Cornes)]

Hello Randy,

> ....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

 The inversion tactic uses some lemmas like sym_eq and f_equal that
are not automatically expanded during Compute. If you make these
lemmas transparent,  then delta expansion is performed and you
obtain the expected computation.

Transparent sym_eq.
Transparent f_equal.

Coq <  Eval Compute in (hdn (consn O (niln nat))).
     = O
     : nat

I hope this helps.

Best regards,
cristina