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.
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.)
