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.