The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Wonchan Lee wrote:
> Definition add (n : nat) (vec : Vec nat (S (S n))) : Vec nat (S n).
> Proof.
>    inversion vec as [| n' x vec'].
>    inversion vec' as [| n'' y vec''].
>    apply (Vec_Cons _ _ (x + y) vec'').
> Qed.
>
> [...]
>
> I wish I can unfold the definition of add in the proof, but it seems not 
> allowed.
>    

Cedric has already explained the problem: ending the definition in [Qed] 
marks it as opaque, i.e. not possible to unfold.

My advice is this: never write program code with tactics (e.g., as 
you're doing for [add] here).  Many people on this list will disagree 
with that advice, but I believe tactics are a proper fit for "proofs" 
only.  For an introduction to the techniques you'll need to avoid using 
tactics to define [add] and similar functions, see CPDT:
    http://adam.chlipala.net/cpdt/