The Coq mailing list

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

Thanks for your reply.  I think I may have given a confusing example, so
let me elaborate.

Here's a head of list function that requires a proof that its input list
has at least one element:

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.

To use this function on a given list, it is necessary to construct a proof
that the list has at least one element:

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

Now, we can take the hd of l:

Eval compute in (hd nat l prp).
     = 1
     : nat

What I am trying to figure out is if it is possible to write something
like the following (please excuse my newbie syntax):

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.  Currently, I have to either write a term for ?? by hand as I'm
writing the definition of f, or I have to replace ?? with a variable and
then define that variable after I've written f.

Does this make sense?  Any thoughts are greatly appreciated.

Regards,
Ryan


> Le Thu, 22 Feb 2007 18:23:04 -0500,
> "Ryan J. Wisnesky" 
>Â <ryan AT eecs.harvard.edu>
>  a écrit :
>
>> Hello,
>>
>> I'm wondering if there is a way to automatically switch between
>> writing a term and the interactive theorem proving mode.  That is, I
>> have a function that takes as an argument a proof that some condition
>> holds; when I'm writing a program that uses this function, I need to
>> construct proofs "on the fly" while writing other functions.  In
>> other words, I have something like
>>
>> Definition f (A B:Set) (pf: A->B) : .. := ....
>
> You can define a function with tactics by no giving its definition:
>
> Definition f (A B:Set) (pf: A->B) : ..  .
> intros.
> ...
> Defined.
>
> Don't forget to end the definition by "Defined" otherwise the function
> body will be hidden.
>
> Once in the tactic mode you can use the refine tactic.
>
> So I would say that you can do the following:
>
> Definition h : <typofh>.
> refine
>   (let g f nat nat _ in
>    complicated thing).
> (* Here you should left with the proof that A->B *)
> Defined. (* not Qed.*)
>
> Cheers
> Pierre Courtieu
>
>
>> later, I want to use this function:
>>
>> Definition h = let g = f nat nat (proof for nat->nat) in complicated
>> thing
>>
>> Right now, I can declare a term x and write
>>
>> let g = f nat nat x in something.
>>
>