Getting start with Proof Market

About Proof Market

Proof Market (https://proofmarket.org) is a web site for theorem providers and theorem provers. Theorem providers submit theorems to be proved with Coq and theorem provers offer their proofs with some price as bounty.

The currency used in this market is BitCoin. A BitCoin address and a amount of BitCoin money are needed when submitting a proof. To read the proof costs a specified amount of BitCoin money.

How to prove theorems and submit proofs

  1. Choose a theorem from Problem List.

  2. Make a directory for the problem.

  3. Copy contents from the Definitions section and save these as a file Definitions.v. Similarly, Answer.v from the Answer Template section, Verify.v from the Verifier section.

    As a Result, directory structure is shown as folloing:

    <Problem Name>/
      Answers.v
      Definitions.v
      Verify.v
    

    If there is no Definition section in the problem page, Definitions.v is not needed.

  4. Write a proof.

    If the last line of an Answer Template is “Admitted.” which means I have not completed the proof, you should change the line into “Qed.” which means I have completed the proof.

  5. Verify the proof.

    ## goto the problem directory
    $ cd <Problem Name>
    
    ## compile Definitions.v if exists
    $ coqc Definitions.v
    
    $ coqc Answer.v
    $ coqc Verify.v
    ## if Verify.v depends on Definitions.v, a require option is needed
    ## $ coqc -require Definitions Verify.v
    
    $ coqchk -o -norec Answer
    

Using ProofGeneral

At the process “4. Write a proof.”, you can use your favorite editors or IDEs. I use ProofGeneral (http://proofgeneral.inf.ed.ac.uk), because I love Emacs.

  1. Progress one step

    C-c C-n

  2. Progress steps until curser position

    C-c C-Enter

  3. Make compilation automatic

    If Verify.v depends on Definitions.v, it is convenient to enable automatic compilation.

    c.f. http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual+%28latest+release%29&file=releases%2FProofGeneral-latest%2Fdoc%2FProofGeneral%2FProofGeneral_12.html#Customizing-Coq-Multiple-File-Support

    From menu-bar, click Proof-General -> Advanced -> Customize -> Coq -> Coq Auto Compile -> Coq Compile Before Require....

Happy proving!!