Coq while trying to use Case. Example from Software Funds

Question

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

I use the interactive command line Coq-interpreter coqtop .

In the induction chapter ( http://www.cis.upenn.edu/~bcpierce/sf/Induction.html ) I follow the instructions exactly. I am compiling Basics.v using coqc Basics.v . Then I start coqtop and print for sure:

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

Everything works to the last line, after which 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 unpacking why this doesn't work. I found something online, suggesting I first make a Require String. but that didn't work either. Has anyone worked on this book or run into this problem? How to make the code work correctly?

This Case keyword (tactics?) Seems to depend on something else that the SF book is not clear, but I can't figure that out.

Answer 1

What is missing is a string data type that binds to the notation "..." ; the String module contains this notation and data type, but you must tell Coq to use this notation with Open Scope string_scope. However, there is also no Case implementation that will be displayed only after fixing the problem line. All this is provided to you in the Induction.v file inside the Tar file of the Download, but it is not included in the output of Induction.html , possibly due to a typo in the .v file. The corresponding code, which will be the second paragraph of the " Case Names" section (immediately after "... but the best way is to use Case tactics" and right before "Here is an example of using Case ..."):

 (* [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. 

(Note: When I worked through Software Foundations, I found that I provided the .v files as my working material is very useful. You do not need to worry about the code released, you do not need to repeat the definitions, and all problems are here. Your mileage may vary , of course.)