The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

Thanks for the advice.  I wasn't aware of this feature. Bullets look very useful and I imagine would make proofs much more readable.

-Fred

On Sat, Nov 14, 2015 at 5:46 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

Congratulations!

I see that your proof script do not use billets (- + * { }).
Use bullets!

Bullets are the one most important change of Coq 8.4 in terms of readability and maintenability of proof scripts. Bullets make the structure of your scripts more readable, but, even more importantly, they make it significantly easier to figure where you are when a proof breaks because you changed a definition or tactic it uses.

See an introduction of bullets in

  http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html

There are several ways to use bullets and it's best to experiment on your own to see what you like (any style is better than no bullets). My current choice is:

- use increasing bullet levels (-, then +, then *) for hierarchy, avoid nesting more than three levels.

  (Jacques-Henri Jourdan remarked that a good way to cut on the nesting is to start with an assert, which encourages forward reasoning in larger proofs, which is arguably a good thing.)

- use braces around "side proofs", typically after an assert.
  Bullets are to be used whenever a tactic creates several subgoals that are on equal footing. For tactics that have one or several "side-proofs" and one "main continuation of the argument", use braces around the side-proofs and continue the argument at the same indentation level.

Use bullets!

On Sat, Nov 14, 2015 at 11:36 PM, Fred Smith <fsmith1024 AT gmail.com> wrote:

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