The Coq mailing list

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

This sound interesting. 

By the way, it appears the solution proposed by Jean-Christophe is restricted:
the "Abort" generates an error message (and stop further processing) at compile
time.

J-Y.


Claude Marche wrote:
> > > > > > "Jean-Christophe" == Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr> writes:
> > > > > >           
> > > > >         
> > > >       
> > >     
> >   
>
>     >> 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
>
> The solution proposed by Jean-Christophe is good for that purpose. For
> collaborative work, it seems to me it is useful to allow
> unproved propositions to be used later. In such case, a trick is to use a
> tactic based on an unsound axiom:
>
> Axiom I_am_unsound_do_not_use_me : False.
> Tactic definition Admitted := Case I_am_unsound_do_not_use_me.
>
> Then 'Admitted' will solve any goal magically...
>
> Hope this helps,
>
>     >> Feasibility ?  Doesn't seems unrealistic, is it ?
>
>     Jean-Christophe> It  seems that  replacing  "Qed" with  "Abort"  in a  proof script  is
>     Jean-Christophe> exactly achieving this goal: the partial proof script is checked until
>     Jean-Christophe> the "Abort" but the lemma is not saved thus cannot be used.
>
>     Jean-Christophe> 	Lemma my_conjecture : ...
>     Jean-Christophe> 	Proof.
>     Jean-Christophe> 	  proof script tentative.
>     Jean-Christophe> 	  ...
>     Jean-Christophe>         Abort.
>
>     Jean-Christophe> -- 
>     Jean-Christophe> Jean-Christophe
>
>     Jean-Christophe> --------------------------------------------------------
>     Jean-Christophe> Bug reports: http://coq.inria.fr/bin/coq-bugs
>     Jean-Christophe> Archives: http://pauillac.inria.fr/pipermail/coq-club
>     Jean-Christophe>           http://pauillac.inria.fr/bin/wilma/coq-club
>     Jean-Christophe> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--

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