The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le vendredi 23 février 2007 00:23, Ryan J. Wisnesky 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) : .. := ....
>
> 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?

This is possible using the Program tactic I developed in v8.1, by writing:
Program Definition h = let g := f nat nat _ in ...

It will generate an obligation to show that (nat -> nat) in the appropriate 
context (actually, it may not be exactly the one you'd expect, but that's 
another problem). You can prove the obligation using:
Next Obligation.
<script>
Qed or Defined depending if you want inlining or not (definitely Defined if 
it 
is used in a Fixpoint definition). Once all obligations are solved you get a 
usual Coq definition. There is a short documentation in the manual describing 
the commands.

Disclaimer: you may encounter a bug, but I'd be glad to hear about it !
-- 
Matthieu Sozeau
http://www.lri.fr/~sozeau