The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

>>>>> "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

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |