The Coq mailing list

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

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) : .. := ....

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.

and then I can prove x separately.  The downside of this is that I have to reassume the context 
where x appears.  Is there any way to switch into theorem proving mode while defining a function, or 
to somehow but in a bunch of "placeholders" and then prove the theorems later, and the have the 
proofs inlined, so as not to need break the proofs out as separate terms but still be able to take 
advantage of the interactive prover?

Thanks,
Ryan Wisnesky