The Coq mailing list

["Ryan J. Wisnesky" <ryan AT eecs.harvard.edu>]

The Program tactic commands seem to be exactly what we want.  From the
reference manual for 8.1:

"The goal of Program is to program as in a regular functional
programming language whilst using as rich a specification as desired and
proving that the code meets the specification using the whole Coq proof
apparatus."

Perfect.  Thanks to everyone for their help.  

Cheers,
Ryan

On Tue, 2007-02-27 at 11:54 +0100, frédéric BESSON wrote:
> Hello,
> 
> As already shown by Laurent Thery, refine does the job.
> Personnaly, I have just discovered Program and like it very much!
> I cannot resist; here is the script.
> 
> (Note that Program does not require a dependant match to accept hd -  
> very nice.)
> 
> Program Definition hd (A:Set) (l : list A) : forall (H : (length l >  
> 0)%nat), A :=
>    fun H =>
>      match l with
>        | nil    => _ (* Here a proof that it cannot happen *)
>        | a :: _ =>  a
>      end.
> Next Obligation.
> apply False_rec.
> compute in H ; omega.
> Qed.
> 
> Program Definition head (l: list nat) : option nat :=
> if zerop (length l) then None else
>    Some (hd nat l _).
> (* Trivial proof obligation discharged by auto *)
> 
> --
> Frédéric Besson