coq hatası. Yazılım Temelleri kitabı

Question

den Örnek I çevrimiçi Yazılım Temelleri kitap aracılığıyla çalışarak Coq öğrenmeye çalışıyorum: Ben interaktif komut satırı Coq tercüman coqtop kullanıyorum http://www.cis.upenn.edu/~bcpierce/sf/

.

İndüksiyon bölümünde (http://www.cis.upenn.edu/~bcpierce/sf/Induction.html), talimatları tam olarak takip ediyorum. Basics.v dosyasını coqc Basics.v kullanarak derlerim. Sonra coqtop başlayıp tam yazın:

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

Her şey, bu son satırı kadar çalışıyor bu noktada ben şu hatayı alıyorum:

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

neden paketten başlamak Coq için çok yeniyim Bu çalışmıyor. İlk önce Require String. yapmam gerektiğini öneren bir şey buldum, ancak bu işe yaramadı. Bu kitapta çalışan veya bu sorunla karşılaştı mı? Düzgün çalışması için kodu nasıl alabilirim?

Bu Case anahtar sözcüğü (taktik?), SF kitabının açıklığa kavuşmadığı başka bir şeye bağımlı gibi görünüyor, ama ne olduğunu anlayamıyorum.

Answer 1

Eksik olan, "..." notasyonuna giren bir dize veri türü; String modülünde böyle bir notasyon ve veri türü vardır, ancak Coq'a bu notasyonu Open Scope string_scope. aracılığıyla kullanmasını söylemeniz gerekir. Ancak eksik olan, Case'un bir uygulamasıdır, bu yalnızca dize problemini düzelttikten sonra görünecektir. Tüm bunlar, "Download" paketinin içindeki Induction.v dosyasında sağlanmıştır, ancak .v dosyasındaki bir yazım hatası nedeniyle Induction.html çıkışına dahil edilmemiştir. İlgili kod, "Adlandırma Kutuları" bölümünün ikinci paragrafı olacaktır (sağdan sonra "… ama daha iyi bir yol Case taktiğini kullanmaktır" ve hemen önce "İşte burada Case'un nasıl kullanıldığına dair bir örnek…") :

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

(bir yan not:. Ben Yazılım Vakıflar aracılığıyla çalıştı, ben çok yardımcı olmak için benim çalışma malzemesi olarak sağlanan .v dosyalarını kullanarak bulundu sen 'don, elided kodu hakkında endişelenmenize gerek yok Tanımları yeniden yazmalı ve tüm problemler tam burada olmalı. Yolculuğunuz değişebilir, elbette.)