errore coq quando si tenta di utilizzare Case. Esempio da Software Foundation libro

Question

sto cercando di imparare Coq lavorando attraverso la linea libro Software Foundation: http://www.cis.upenn.edu/~bcpierce/sf/

sto usando la linea di comando interattivo Coq interprete coqtop.

Nel capitolo di induzione (http://www.cis.upenn.edu/~bcpierce/sf/Induction.html), sto seguendo esattamente le istruzioni. Compilare Basics.v utilizzando coqc Basics.v. Ho poi comincio coqtop e digitare esattamente:

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

Tutto funziona fino a quella ultima riga, a quel punto ho il seguente errore:

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

Sono troppo nuova per Coq per iniziare a disfare perché questo non funziona Ho trovato qualcosa online che suggeriva di aver bisogno di fare Require String. prima, tuttavia, questo non ha funzionato neanche. Qualcuno ha lavorato a questo libro o ha riscontrato questo problema? Come faccio a far funzionare correttamente il codice?

Questa parola chiave Caso (tattica?) Sembra dipendere da qualcos'altro che il libro SF non sta rendendo chiaro è necessario, ma non riesco a capire cosa.

Answer 1

Quello che manca è un tipo di dati stringa che si aggancia alla notazione "..."; il modulo String contiene tale notazione e tipo di dati, ma devi dire a Coq di usare quella notazione tramite Open Scope string_scope. Ciò che manca, tuttavia, è un'implementazione di Case, che verrà visualizzata solo dopo aver risolto il problema di stringa. Tutto questo è fornito nel file Induction.v all'interno del tarball "Download", ma non è incluso nell'output Induction.html, probabilmente a causa di un refuso nel file .v. Il codice pertinente, che sarebbe il secondo paragrafo della sezione "Casi di denominazione" (subito dopo "... ma un modo migliore è utilizzare la tattica Case" e subito prima "Ecco un esempio di come viene utilizzato 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. 

(Una nota a margine:. Quando ho lavorato attraverso Software Foundation, ho trovato utilizzando i .v file forniti come il mio materiale di lavoro per essere molto utile non vi dovrete preoccupare di codice eliso, si don' Devo ridigitare le definizioni, e tutti i problemi sono proprio lì. Il tuo chilometraggio può variare, ovviamente.)