The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

Dear all,

what do you think of the following suggestion, I think feasible, from the
Coq's developers point of view ;>)

We have "Lemma", "Theorem", "Axiom" and "Remark".

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 ?

Cheers

Jean-Yves

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com