coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Wonchan Lee <wclee AT ropas.snu.ac.kr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] unfold definition on vectors
- Date: Mon, 19 Dec 2011 09:20:02 -0500
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/
- [Coq-Club] unfold definition on vectors, Wonchan Lee
- Re: [Coq-Club] unfold definition on vectors, AUGER Cédric
- Re: [Coq-Club] unfold definition on vectors, Adam Chlipala
- Re: [Coq-Club] unfold definition on vectors,
AUGER Cédric
- Re: [Coq-Club] unfold definition on vectors, Adam Chlipala
- Re: [Coq-Club] unfold definition on vectors,
AUGER Cédric
Archive powered by MhonArc 2.6.16.