coqエラーが発生しました。例ソフトウェア財団帳

Question

から私は、オンラインソフトウェア財団ブックを通じて働くことによってコックを習得しようとしています：http://www.cis.upenn.edu/~bcpierce/sf/

私は対話型のコマンドラインコックインタプリタcoqtopを使用しています。

誘導の章（http://www.cis.upenn.edu/~bcpierce/sf/Induction.html）では、指示に正確に従っています。私はcoqc Basics.vを使ってBasics.vをコンパイルします。私はその後、coqtopを起動して、正確に入力します。

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

すべてが、私は次のエラーを取得するその時点でその最後の行まで動作します：

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

私は理由を解凍するために開始するコックにあまりにも新たなんですこれは動作していません。私はRequire String.を最初にやる必要があると提案した何かをオンラインで見つけましたが、これはうまくいきませんでした。誰かがこの本を読んだりこの問題に遭遇しましたか？コードを正しく動作させるにはどうすればよいですか？

このCaseキーワード（戦術？）は、SFの本が明らかにしていないものに依存しているように見えますが、何が分かりません。

Answer 1

欠けているものは、"..."表記にフックする文字列データ型です。 Stringモジュールにはそのような表記法とデータ型が含まれていますが、CoqにOpen Scope string_scope.という表記法を使用するように指示する必要があります。Caseの実装は文字列の問題を修正した後にのみ表示されます。これらのすべては "ダウンロード" tarballの中のInduction.vファイルで提供されますが、.vファイルのタイプミスのために出力Induction.htmlに含まれていません。 "Naming Cases"セクションの第2段落（「...より良い方法はCaseの戦術を使用することです」の直後、「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. 

（サイドノート：私はソフトウェア財団を通じて働いていたとき、私は非常に有用であることが私の仕事の材料として提供.vファイルを使用していますが、「あなたはドン、省略さコードを心配する必要はありません。定義を再入力する必要があり、そこにすべての問題があります。もちろん、あなたの走行距離は変わるかもしれません。）