First Chapter of Software Foundations: Basics: Functional Programming in Coq

  • March 10, 2014 · 7:00 PM
  • Mixrank

Let's do the exercises in the first chapter of "Software Foundations" (by Benjamin Pierce and a whole bunch of other people) and then get together and discuss it.

You'll need to do a fair amount of system administration before you get started:

. downloading the book . installing Coq . installing emacs . installing the Proof General plugin for emacs

Also strongly recommended is to download a copy of Adam Chilpala's "Certified Programming with Dependent Types"; I would skim through the first two chapters before starting with Software Foundations, because Chilpala gives an overview of how Coq is put together and what Coq can do that makes the beginning of Software Foundations a lot less mysterious.

Details:

. Download Software Foundations (henceforth "SF") from http://www.cis.upenn.edu/~bcpierce/sf/ (I'm not aware of a paper edition). Untarring it gives you a directory of .html files (browsable) and .v files, which are the literate Coq source files for the book. In order to do the exercises, you actually modify the .v files.

The chapters in SF aren't numbered and vary in length, but the first real chapter (the one we're doing for this meeting) is the one titled "Basics: Functional Programming in Coq".

. Install Coq from http://coq.inria.fr/download (current version is 8.4pl3).

You can interact with Coq using coqtop on the command line, or through Proof General in an emacs buffer. Because most things you do with Coq are many lines long, coqtop isn't very helpful unless you want to do something really simple.

. Install emacs (if you don't already have it; from http://www.gnu.org/software/emacs/). You'll want version 23.3 or later (current version is 24.3) for compatibility with Proof General.

If you haven't used emacs before, I'm afraid this may be a bit of a culture shock. emacs probably has modes that emulate almost any text editor you might be familiar with, but I'm afraid I don't know much about them.

. Install Proof General from http://proofgeneral.inf.ed.ac.uk/download (current version is 4.2). Note that you have to edit your ~/emacs.d file to make emacs able to find Proof General, so follow all the installation instructions!

I've found the Proof General documentation to be rather unapproachable, but so far there's really only one command I've needed. To get Proof General to process a Coq source buffer, position your cursor in the buffer at the point up to which you'd like Proof General to run Coq, and type CTRL-C CTRL-ENTER.

. Chilpala's "Certified Programming with Dependent Types" is available in both paper and PDF editions (the PDF is free!) from http://adam.chlipala.net/cpdt/ .

Join or login to comment.

  • Sergei W.

    I found a rather artificial proof for this lemma, where I had to declare a function (can I do this inside the proof?). Perhaps I am missing something.

    Definition nat_const_of_bool(b:bool):nat :=
    match b with
    | true => 1
    | false => 0
    end.

    Lemma nonsense1: true=false -> 0=1.
    Proof. intros H.
    replace (1) with (nat_const_of_bool true).
    replace (0) with (nat_const_of_bool false).
    rewrite -> H. reflexivity. reflexivity. reflexivity.
    Qed.

    March 13, 2014

  • Sergei W.

    One thing that bothered me about some proof techniques is the necessity of deriving nonsense from nonsense. For example, if you want to prove that some property P(n) holds when n is even, Theorem A: is_even n = true -> P(n)=true.

    and you use induction in n, you will have to derive is_even (n) -> P(n) also for odd n. In other words, you will have to derive P(n) from falsehood. I found that it's not so easy to derive things from falsehood! Here is a basic lemma that would be quite useful

    Lemma nonsense1: true = false -> 0 = 1.
    Proof. ???

    In classical logic, anything follows from falsehood. But we are not in classical logic. There is no notion of a theorem that is false; only a theorem that is not yet proven. In the intuitionistic logic, "true=false" is merely a theorem for which we have no proof.

    March 13, 2014

  • Sergei W.

    Another beautiful error message from Coq while trying to define a recursive function:

    (* will return false in any case *)
    Fixpoint foo (f:bool) : bool :=
    match f with
    | false => false
    | true => foo false
    end.

    Error:
    Recursive definition of foo is ill-formed.
    In environment
    foo : bool -> bool
    f : bool
    Recursive call to foo has principal argument equal to
    "false" instead of a subterm of "f".
    Recursive definition is:
    "fun f : bool => match f with
    | true => foo false
    | false => false
    end".

    March 11, 2014

  • Juan P.

    The coq download link appears non-functional.

    March 10, 2014

    • Sergei W.

      Sorry, I guess I was too optimistic... It seems they only support syntax highlighting for Coq.

      March 10, 2014

    • Sergei W.

      http://proofweb.cs.ru...­ Look for "Proof assistants on the Web" and click "guest login" to Coq

      March 10, 2014

  • Brandon

    I'm leaving from the Redwood City area if anyone wants a ride up.

    March 10, 2014

  • Ian Z.

    Doing the last exercise (binary numbers) I seem to be stuck on arithmetic. I got as far as

    n + 1 + (n + 1) = n + n + 1 + 1

    but don't know how to make progress from there, even after importing Coq.Arith.Plus.

    March 9, 2014

    • Adrian K.

      I don't think the book was actually asking us to prove this at this point: it says "notice that...", not "prove that...". It looks as if we're supposed to know enough to prove it after the next chapter (on induction).

      March 9, 2014

    • Adrian K.

      As for a faster way, it is, after all, software "foundations".­ Build your universe atom by atom.

      March 9, 2014

  • Ian Z.

    Reading the book as HTML, is there any reason for the style which squashes everything into a strip on the left occupying less than 1/3 of my available screen width?

    March 8, 2014

    • Adrian K.

      You know, I was wondering that too. But you have the source (.v) file from which the .html was generated, so I suppose you could just write another HTML generator that lays it out differently.

      March 9, 2014

  • A former member
    A former member

    If you'd rather use vim, try this: https://github.com/the-lambda-church/coquille

    March 8, 2014

  • Sergei W.

    Another thing: the whole book is written out as comments in the .v files. Exercises are done by editing the same .v files. So it is sufficient just to have an Emacs buffer with these files; no need to look at the book, and no need for PDF of that book.

    March 8, 2014

  • Sergei W.

    I am also using Mac OS X, now installed "Aquamacs", compiled Coq, having some minor problems with compiling Proof General's elisp files (fails to compile support for HOL/Isar), but so far the Coq part of Proof General seems to work.
    Found this video to be helpful,
    http://www.youtube.com/watch?v=l6zqLJQCnzo
    It's odd that neither of the books (Chlipala or Pierce et al.) explain how to run Coq on what you write in Emacs. This is "C-c C-n" or "Next step" in the menu. Not obvious.

    March 8, 2014

  • Ted F.

    Hi Adrian et al.,

    Here is an update specifically for us (unfortunate) OSX Mavericks users:

    If you are using something like a Macbook Pro, the <C-ENTER> command can't be done without some modifications. A resource is provided at this site but it involves downloading some extra apps: http://xahlee.info/kbd/Mac_OS_X_keymapping_keybinding_tools.html
    This is extra work that may need to be done if you want to use proof general.

    The standalone OSX CoqIDE app does not seem to be a viable option for Mavericks users: https://coq.inria.fr/bugs/show_bug.cgi?id=3155

    My current (only) solution: Homebrew to the rescue! Homebrew-formal (https://github.com/mht208/homebrew-formal) can initialize CoqIDE using the command line. Just follow the "brew tap" instructions and do "brew install coqide". It seems to be working so far.

    If anyone else has a more convenient solution, I'd really appreciate it!

    February 28, 2014

  • Ted F.

    Hi All,

    Looking forward to learning Coq, but is emacs/proof general necessary to follow SF? I'm currently experiencing the emacs culture shock which is probably worse for me since I am, at best, a vim novice. I found an old vim CoqIDE emulator but I'm not sure if it is working. I'm guessing the real CoqIDE is insufficient for SF?

    February 26, 2014

    • Adrian K.

      I haven't tried CoqIDE myself; I'm following Chilpala's advice in choosing the emacs/Proof General combination. If you want to trailblaze with CoqIDE or the vim emulator and figure out whether either of those works well (or works with what caveats), that would be useful to know.

      February 27, 2014

  • Sergei W.

    yes, looking forward to the first steps in formalized programming... As for the amount of computer preparation -- at least this is something you compile, install, and run, i.e. work is done by the computer, rather than twenty-three academic papers you need to read yourself, with your single-threaded, battery-operated brain...

    February 22, 2014

    • Adrian K.

      Oh, yours uses batteries? Mine runs on caffeine.

      February 22, 2014

  • Christopher B.

    The Coq'Art book is also helpful for getting oriented. Unfortunately the only online versions are French and Chinese (http://www.labri.fr/perso/casteran/CoqArt/). For $80 you can order hardback in English from Amazon (http://www.amazon.com/Interactive-Theorem-Proving-Program-Development/dp/3540208542/ref=sr_1_1?s=books&ie=UTF8&qid=1392422179&sr=1-1&keywords=coq+art)

    February 14, 2014

People in this
Meetup are also in:

Imagine having a community behind you

Get started Learn more
Henry

I decided to start Reno Motorcycle Riders Group because I wanted to be part of a group of people who enjoyed my passion... I was excited and nervous. Our group has grown by leaps and bounds. I never thought it would be this big.

Henry, started Reno Motorcycle Riders

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy