The Coq mailing list

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

Ooooops, forget my last remark. The error came form the "Qed" after the 
"Abort", sorry for the noise.
JY

Jean-Yves Vion-Dury wrote:

> 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 
> <http://www.xrce.xerox.com/people/vion-dury/home.html>   /Research 
> Scientist/     * Xerox Research Centre Europe *
> *INRIA* (sabbatical)
> 655 avenue de l'Europe,
> 38334 Montbonnot (FRANCE)
> Jean-Yves.Vion-Dury AT inrialpes.fr 
> <mailto: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 <http://www.alphaAve.com>

--
Jean-Yves Vion-Dury 
<http://www.xrce.xerox.com/people/vion-dury/home.html>   /Research 
Scientist/     * Xerox Research Centre Europe *
*INRIA* (sabbatical)
655 avenue de l'Europe,
38334 Montbonnot (FRANCE)
Jean-Yves.Vion-Dury AT inrialpes.fr 
<mailto: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 <http://www.alphaAve.com>