coq error when trying to use Case. Example from Software Foundations book -

i trying learn coq working through online software foundations book: http://www.cis.upenn.edu/~bcpierce/sf/

i'm using interactive command line coq interpreter coqtop.

in induction chapter (http://www.cis.upenn.edu/~bcpierce/sf/induction.html), following instructions exactly. compile basics.v using coqc basics.v. start coqtop , 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 last line, @ point following error:

toplevel input, characters 5-15: > case "b = true". >      ^^^^^^^^^^ error: no interpretation string "b = true". 

i'm new coq start unpack why isn't working. found online suggesting needed require string. first, however, didn't work either. has worked through book or encountered problem? how code work properly?

this case keyword (tactic?) seems dependent on else sf book not making clear needed, can't figure out what.

what's missing string datatype hooks "..." notation; string module contains such notation , datatype, have tell coq use notation via open scope string_scope. what's missing, however, implementation of case, show after fix string problem. of provided in induction.v file inside "download" tarball, not included in output induction.html, possibly due typo in .v file. relevant code, second paragraph of "naming cases" section (right after "…but better way use case tactic," , right before "here's example of how case used…") is:

(* [case] not built coq: need define ourselves.     there no need understand how works -- can skip     on definition example follows.  uses     facilities of coq have not discussed -- string     library (just concrete syntax of quoted strings) ,     [ltac] command, allows declare custom tactics.  kudos     aaron bohannon nice hack! *)  require string. open scope string_scope.  ltac move_to_top x :=   match reverse goal   | h : _ |- _ => try move x after h   end.  tactic notation "assert_eq" ident(x) constr(v) :=   let h := fresh in   assert (x = v) h 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 working on 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 worked through software foundations, found using provided .v files work material helpful. don't have worry elided code, don't have retype definitions, , problems right there. mileage may vary, of course.)