The Coq mailing list

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

Le Mon, 19 Dec 2011 09:20:02 -0500,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

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

Adam, does the refine tactic falls in the "never write program code
with tactics"?

I sometimes do things like (not real code though):
>>>
Fixpoint f x : {y:nat | P x y}.
refine (
  match x with
  | A x t => {: ν(f x)+t (*labeled proof*):}
  end
).
Proof.(*labeled proof*)
 abstract (clear - x t; auto).
Defined.
<<<
where ν is the witness of the "{x|P x}" type
and {:x:} is a notation for (existT _ x _(*proof to be done*))

I find it really convenient since I can express in a clean way all the
computationnal part and have proofs separated (I know that "Program"
does a similar thing for no particular reason).