The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le Mardi 27 Février 2007 10:54, frédéric BESSON a écrit :
> 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.)

Actually, one is happening behind the scene so the obligations have the 
proper 
equalities in their context (it works with dependent types in the svn version 
only).

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

We can do even better:

Require Import Coq.subtac.Utils.
Variable A : Type.

Program Definition head  ( l : list A | length l  <> 0 ) : A :=  
  match l with
        | nil  => !
        | hd :: tl  => hd
  end.

Here ! is a notation for (False_rect _ _).
(* Proof automatically discharged by a default tactic. *)

> 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 *)

> Program Definition head (l: list nat) : option nat :=
> if zerop (length l) then None else
>    Some (hd nat l _).

Program Definition head_option (l: list A) : option A :=
  if zerop (length l) then None else Some (head l).
-- 
Matthieu Sozeau
http://www.lri.fr/~sozeau