Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] unfold definition on vectors

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unfold definition on vectors


chronological Thread 
  • 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/




Archive powered by MhonArc 2.6.16.

Top of Page