The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

I'm surprised Gérard did not mention it. There used to be a Qed "song"
long time ago around 1991-1993 in the versions 5.6 to 5.8.

I attach the file!

Hugo

On Sat, Nov 12, 2011 at 01:42:26PM -0500, Alexandre Pilkiewicz wrote:
> 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
> >
> >
>

Attachment: rooster.au
Description: Basic audio