The Coq mailing list

[Wonchan Lee <wclee AT ropas.snu.ac.kr>]

Hello list,

I'm curious about how to unfold definitions defined on vectors.
Here is my code snippet and I got stucked at the last lemma:

Inductive Vec (A : Set) : nat -> Set :=
| Vec_Nil : Vec A O
| Vec_Cons : forall n, A -> Vec A n -> Vec A (S n).

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.

Lemma add_correct : forall (n : nat) (xs : Vec nat n) (x y : nat),
  add _ (Vec_Cons _ _ x (Vec_Cons _ _ y xs)) =
  Vec_Cons _ _ (x + y) xs.
Proof.
  (* get stucked *)

I wish I can unfold the definition of add in the proof, but it seems not 
allowed.
Is there any tactic working on this case?
Or, do I need a different approach?

Best Regards,
Wonchan Lee