The Coq mailing list

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

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