The Coq mailing list

[fr�d�ric BESSON <fbesson AT irisa.fr>]

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