The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Mon, 26 Feb 2007 14:29:22 -0500 (EST),
"Ryan J Wisnesky." 
<ryan AT eecs.harvard.edu>
 a écrit :

> Definition f (l2: list nat) : option nat :=
>   if length l2 > 0
>     just (hd nat l2 ??)
>   else
>     nothing
> 
> In this definition, ?? needs to be a proof that the length of l2 is
> greater than 0.  Ideally, because this proof occurs inside an if
> branch where length l2 > 0 is true, I'd like to automatically enter
> the theorem prover and trivially show that l2 is true in this
> context, or, to replace ?? with a variable corresponding to a
> verification condition to be proven later. 

As I said in my previous mail you can define a function *interactively*
(meaning: "with tactics"). Then you can define your function *by term*
using the tactc named "refine". 

HerBelow is the script for your example (M. Sozeau Solution may be even
better actually). If this is not what you want please develop.
Cheers,
Pierre Courtieu


Require Import List.
Require Import Le.

Definition hd (A:Set) (l : list A) :=
   match l return (length l > 0 -> A) with
   | nil    => fun H : length nil > 0 => False_rec A (le_Sn_O 0 H)
   | a :: _ => fun _ => a
   end.

Definition l := cons 1 nil.

Definition prp : length l > 0 := le_n 1.

Eval compute in (hd nat l prp).

Require Import Arith.

Definition f (l2: list nat) : option nat.
Proof.
  intro l2.
  refine 
    (if (le_lt_dec (length l2) 0)
      then None
      else Some (hd nat l2 _)).
  auto.
Qed.