The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

 > what about offering "Conjecture":
 > 
 >    1.  Such propositions could not be used  (of course) in other proofs,
 >       but...
 >    2. The coq compiler would accept incomplete proofs and still check
 >       for the correctness of what is present
 > 
 > Interest ?:
 > 
 >    1. Offers handling of partial but correct proof developments
 >       (especially for long and difficult proofs)
 >    2. Enables maintaining of incomplete work (it is usually done through
 >       comments, thus not sensitive to contextual changes)
 >    3. helps collaborative work
 > 
 > Feasibility ?  Doesn't seems unrealistic, is it ?

It  seems that  replacing  "Qed" with  "Abort"  in a  proof script  is
exactly achieving this goal: the partial proof script is checked until
the "Abort" but the lemma is not saved thus cannot be used.

        Lemma my_conjecture : ...
        Proof.
          proof script tentative.
          ...
        Abort.

-- 
Jean-Christophe