The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Ah, I realize I wasn't clear! The Qed. went through, my Theorem was
defined! I'm "complaining" about the after-Qed :)

2011/11/12 Gérard Huet 
<Gerard.Huet AT inria.fr>:
> Qed is indeed the most mysterious of all Coq commands.
> Naive users who have not read the manual don't understand the need to check 
> that the proof is done when the proof is finished.
>
> Once you understand the need, explaining exactly what is done by Qed is 
> only for the brave. Of course, you may always look at the code,
> but at the end of the day you will understand that Qed brings you actually 
> no certainty whatsover.
>
> Either Qed execution stops with satisfaction, and now you know that you 
> have a Coq certified proof. The truth of your purported theorem
> still relies on Coq's consistency, which is not provable in Coq or any 
> strong enough logic to express this statement, unless it it is
> itself inconsistent, by virtue of Gödel's 2nd incompleteness theorem.
>
> Or else Qed execution stops with some failure statement, typically 
> indicating universes inconsistency. This could mean that your
> purported theorem is false, but this could also just mean that although 
> your theorem is valid, it is not provable within
> Coq's formal system, due to lack of universe polymorphism or other. We know 
> anyway that some truths must escape Coq, unless Coq
> is inconsistent, by Gödel's theorem again.
>
> The last case is when the system never returns. But again nothing is 
> learned, because how do you know it will actually never return ?
> Maybe Alexandre has not been patient enough. To wait either for some 
> resource exhaustion OS termination, or to power failure or
> other natural crash of the hardware. Who knows, Alexandre might be dancing 
> at that time, instead of giving up.
>
> In brief, Qed gives no information, and the naive user may be right after 
> all.
> Gérard
>
> PS. Of course Qed is essential, since it allows quick debugging of your 
> conjectures using tactics driving an inconsistent logic.
>
> Le 12 nov. 2011 à 17:03, Alexandre Pilkiewicz a écrit :
>
>> Hi everyone!
>>
>> Yesterday, I realized something big is missing in the coq ecosystem!
>>
>> I just finished a big proof, typed the Qed., waited a few second for
>> the type checking of the term to finish, and then... nothing! I wanted
>> to celebrate, to share my happiness with the world, I wanted to dance.
>> But there is no Qed dance :(
>>
>> I mean, sure, there is the Qt4 dance
>> (http://www.youtube.com/watch?v=NbTEVbQLC8s), but I did not finish a
>> shinny multiplateforme software, I finished a proof!
>>
>> So I think the next step for the evolution of the great piece of
>> software that Coq is is clear: the Coq team needs to give us the Qed
>> Dance!
>>
>> Cheers,
>>
>> Alexandre
>
>