The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

That is wonderful!

-Greg

On Jan 31, 2015, at 11:28 AM, Gérard Huet <Gerard.Huet AT inria.fr> wrote:

In the early days of Coq (1990), my favorite example to show off or teach Coq was the Gilbreath Theorem, due to the magician Gilbreath with his invention of the Gilbreath shuffle trick, an excellent exact card trick, published as: N. Gilbreath. “Magnetic Colors.” The Linking Ring, 38 5 (1959).

N. de Bruijn, who was fond of magic,  had generalized it to a property of binary sequences, which he applied to a problem of crystal theory in:  N.G. de Bruijn. “A riffle shuffle card trick and its relation to quasi crystal theory.” Nieuw Archief Voor Wiskunde 5 3 (1987) 285–301.

Around 1988 Pr. de Bruijn visited my home in Feucherolles, where he did the trick to my 9 year old daughter Isabelle (the one of Isabelle fame). I was intrigued, axomatized the trick in Gallina, and set to prove it formally in Coq. It turned out to be a nice challenge, since the inductive proof needs to go 3 steps deep in the recursion. 

I managed to steer Coq through its then limited automation facilities into an honorable Gallina script, culminating in:

 Gilbreath theorem : (x:word)(even x)->(alternate x)->(u,v:word)(conc u v x)->(w:word)(shuffle u v w)->

                                     if (opposite u v) then (paired w) else (paired (rotate w))

Daniel de Rauglaudre had hacked the card trick as an X-window demo, where cards would fly across the screen in dazzling manner.

After fooling the spectators and challenging them into stating the reason of the amazing result, I would go into the Coq demo, showing the Gallina functionalities

as a mathematical vernacular. I presented Coq at the Types meeting in Edinburgh with the trick. I wrote an article about the experiment which appeared in the Proceedings of the Second Workshop on Logical Frameworks (Edinburgh, May 1991).

I then challenged all automated theorem provers boasting of automating induction to crack the result automatically. It is rumored that J Moore stopped eating and sleeping until he hammered the Boyer-Moore theorem prover to submission. 

I like this demo, because first of all it is sexy and attracts full attention of the audience if you start by doing the trick with real cards. If your audience is mathematically minded, they will venture conjectures that you will show wrong by playing a counter-example. Now you are in business to show Coq in action.

This example was part of the standard Coq user library at the time. It may even have survived, after successive compatibility adjustments. Of course nowadays Coq's automation tools are much more powerful, and most of the lemmas ought to be within automatic reach.

Another positive point is that it motivates mathematics as a powerful tool that has a concrete grasp on reality, all the way from card tricks to crystallography. 

Gérard