The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Mon, 19 Dec 2011 16:36:18 +0900,
Wonchan Lee 
<wclee AT ropas.snu.ac.kr>
 a écrit :

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

That is normal since it is a proof ^^.

Just end "add" with "Defined" (I think "Saved." also works), so it
won't be considered a proof (or more precisely will be set transparent).

Take a look at what opaque/transparent is in the coq reference manual
for more informations.