The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

Hi,

I jus completed my first unguided formalization in Coq.  That is, I formalized a result that I was initially not sure was true, and whose proof was not known to me in advance.

The result concerns a familiar type of puzzle involving scales.  In these puzzles, one is tasked with finding a fake coin amongst a collection of real coins using only a balance scale.  The goal is to use the balance scale as few times as possible.

The just-completed proof shows that the given algorithm is optimal for any number of coins where there is exactly one fake.  The source code and details are here:

           https://github.com/fsmith1024/scales

Although the proof only involves elementary facts, this proof was very challenging for me.  It ends up clocking in at 5000 lines of proof code; far beyond what I expected this exercise to require.

Having no prior exposure to Coq and pursuing this activity in spurts in off hours, most of the proofs are done in  SWAT team style -- what do I need to establish, kick down the door, and flail around hoping that once the dust clears no hypotheses remain. 

Having powered my way through brute force to the finish line, I am now not quite sure what to do with it.  So if you find it amusing, enjoy.  

If you have suggestions for improvement I would welcome those.

Best,

Fred Smith