The Coq mailing list

[David Delahaye <delahaye AT jurancon.inria.fr>]

    Hi Hans,

> - Some of the proofs are too large for Coq. Is there a way of getting 
>    them through? The files Bew_demod.v and Bew_subsunt.v are accepted  
>    up to the point of 'Subtree proved!'. If I type 'Qed.' after that, 
>    Coq computes for several hours, and then crashes. Is there 
>    a way to avoid this? What is it doing? Is it normalizing the proof 
>    term? Can I consider the proof checked when Coq tells 'Subtree 
>    proved!'?

    Big proofs are a thorny problem for Coq. When you obtain "Subtree 
proved!",
you cannot consider that your proof is really checked. The proof tree has to 
be
translated into a term, which allows the consistency of the tree to be
verified, and then, the term has to be typechecked. A tactic can make "silly"
things on a goal and the only way to keep consistency is to build the term and
to verify if its type is the type of your goal.

    Currently, you can try to use "Abstract" in the branches which you "Cut",
but be careful, you have to provide a solving tactic after "Abstract".
"Abstract" saves an intermediate lemma to lighten big proofs. Another 
solution,
may be more drastical for your application, is to create real intermediate
lemmas.

> - Sometimes I receive a message that I need to report something:
> 
> If this is in user-written tactic code, then it needs to be modified.
> If this is in system code, then it needs to be reported.
> 
>    The file Report.v reproduces this message. 

    Yes, you had to report it and you made it! It was a bug concerning 
negative
or nil references in a list of bindings. It is fixed, thank you. However, in
your example, your try to make a binding with a nil reference, which is not
defined.

    Best regards.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[If you have time to waste, you can have a look on my proof that 2=1:

   Given x in R*
   We write: x^2=x+x+...+x, x times
   We derive: 2*x=1+1+...+1, x times
   That is to say: 2*x=x
   As x<>0, we have: 2=1]