Coq-Fehler beim Versuch, Case zu verwenden. Beispiel von Software Foundations Buch

Question

Ich versuche Coq zu lernen, indem sie durch die Online-Software Foundations Buch zu arbeiten: http://www.cis.upenn.edu/~bcpierce/sf/

Ich coqtop die interaktive Kommandozeile Coq-Interpreter.

Im Induktionskapitel (http://www.cis.upenn.edu/~bcpierce/sf/Induction.html) befolge ich genau die Anweisungen. Ich kompiliere Basics.v mit coqc Basics.v. Ich fange dann coqtop und gebe genau:

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

Alles funktioniert, bis die letzte Zeile, an welcher Stelle ich die folgende Fehlermeldung:

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

Ich bin zu neu zu Coq auspacken zu starten, warum das funktioniert nicht. Ich fand etwas online, das vorschlug, dass ich Require String. zuerst tun musste, aber dieses funktionierte auch nicht. Hat jemand dieses Buch durchgearbeitet oder ist dieses Problem aufgetreten? Wie bekomme ich den Code richtig funktioniert?

Dieses Case-Schlüsselwort (Taktik?) Scheint von etwas anderem abhängig zu sein, das das SF-Buch nicht klar macht, aber ich kann nicht herausfinden, was.

Answer 1

Was fehlt ist ein String-Datentyp, der in die "..." Notation einhakt; Das String Modul enthält eine solche Notation und Datentyp, aber Sie müssen Coq sagen, diese Notation über Open Scope string_scope. zu verwenden. Was auch fehlt, ist jedoch eine Implementierung von Case, die nur angezeigt wird, nachdem Sie das String-Problem behoben haben. All dies ist für Sie in der Datei Induction.v innerhalb der "Download" Tarball zur Verfügung gestellt, aber es ist nicht in der Ausgabe Induction.html enthalten, möglicherweise aufgrund eines Tippfehlers in der Datei .v. Der entsprechende Code, der der zweite Absatz des „Naming Cases“ Abschnitt wäre (gleich nach „... aber ein besserer Weg ist es, die Case Taktik nutzen“, und direkt vor „Hier ist ein Beispiel dafür, wie Case verwendet wird ...“) wird

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

(Nebenbemerkung:. als ich durch Software Foundations arbeitete, fand ich die mitgelieferten .v Dateien als mein Arbeitsmaterial mit sehr hilfreich sein Sie müssen nicht über elided Code Sorge, Sie don‘ t müssen die Definitionen erneut eingeben, und alle Probleme sind genau dort. Ihre Laufleistung kann natürlich variieren.)