10

I am trying to learn Coq by working through the online Software Foundations book: http://www.cis.upenn.edu/~bcpierce/sf/

I'm using the interactive command line Coq interpreter coqtop.

In the induction chapter (http://www.cis.upenn.edu/~bcpierce/sf/Induction.html), I am following the instructions exactly. I compile Basics.v using coqc Basics.v. I then start coqtop and type exactly:

Require Export Basics. 
Theorem andb_true_elim1 : forall b c : bool,
  andb b c = true -> b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true".

Everything works until that last line, at which point I get the following error:

Toplevel input, characters 5-15:
> Case "b = true".
>      ^^^^^^^^^^
Error: No interpretation for string "b = true".

I'm too new to Coq to start to unpack why this isn't working. I found something online suggesting I needed to do Require String. first, however, this didn't work either. Has anyone worked through this book or encountered this problem? How do I get the code to work properly?

This Case keyword (tactic?) seems to be dependent on something else that the SF book is not making clear is needed, but I can't figure out what.

1

1 Answer 1

15

What's missing is a string datatype which hooks into the "..." notation; the String module contains such a notation and datatype, but you have to tell Coq to use that notation via Open Scope string_scope. What's also missing, however, is an implementation of Case, which will only show up after you fix the string problem. All of this is provided for you in the Induction.v file inside the "Download" tarball, but it is not included in the output Induction.html, possibly due to a typo in the .v file. The relevant code, which would be the second paragraph of the "Naming Cases" section (right after "…but a better way is to use the Case tactic," and right before "Here's an example of how Case is used…") is:

(* [Case] is not built into Coq: we need to define it ourselves.
    There is no need to understand how it works -- you can just skip
    over the definition to the example that follows.  It uses some
    facilities of Coq that we have not discussed -- the string
    library (just for the concrete syntax of quoted strings) and the
    [Ltac] command, which allows us to declare custom tactics.  Kudos
    to Aaron Bohannon for this nice hack! *)

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

(A side note: When I worked through Software Foundations, I found using the provided .v files as my work material to be very helpful. You don't have to worry about elided code, you don't have to retype the definitions, and all the problems are right there. Your mileage may vary, of course.)

4
  • Cool, thanks, that works perfectly. Pointing me to the induction.v file is really helpful as well, it hadn't occurred to me that there would be code in the v not in the html. So I guess what this means is that Case is not something built into the language, but something added by the SF authors for annotating a proof? Is this a common practice or something peculiar to SF's way of doing things? Also, I'm not sure I understand why the "Case" stuff is better than just a simple comment like (* case b=true *).
    – John
    Commented Oct 6, 2013 at 22:28
  • @quadelirus The Case stuff will throw an error and thereby ease debugging if something changes. Example: If you do induction over nats and your base (O) case's tactics no longer solve that part after a change, it will throw an error on Case "n = S n'" instead of going on and applying the S-case stuff onto the (still unfinished) O-case.
    – nobody
    Commented Oct 14, 2013 at 19:24
  • @quadelirus These Case-markers can be found in developments other than the software foundations, but there are other styles as well. Personally, I prefer "Chlipala style" proving (i.e. automating to the point where the proofs are short enough that you simply don't need any Case markers.) -- see adam.chlipala.net/cpdt for yet another Coq book.
    – nobody
    Commented Oct 14, 2013 at 19:43
  • +1 Thanks for posting this. I was working through the examples and missed this too. Precisely what I needed. Commented May 1, 2014 at 4:59

Not the answer you're looking for? Browse other questions tagged or ask your own question.