尝试使用 Case 时出现 coq 错误。软件基础书籍中的示例

Question

我正在尝试通过在线软件基础书籍来学习 Coq:http://www.cis.upenn.edu/~bcpierce/sf/

我正在使用交互式命令行 Coq 解释器 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".

我对 Coq 太陌生，无法开始解释为什么它不起作用。我在网上发现一些建议我需要首先执行 Require String. ，但是，这也不起作用。有人读过这本书或遇到过这个问题吗？如何让代码正常工作？

这个 Case 关键字(策略？)似乎依赖于 SF 书没有明确说明的其他东西，但我不知道是什么。

Answer 1

缺少的是与 "..." 表示法 Hook 的字符串数据类型； String 模块包含这样的表示法和数据类型，但您必须通过 Open Scope string_scope 告诉 Coq 使用该表示法。 然而，还缺少 的实现code>Case，只有修复字符串问题后才会显示。所有这些都在“下载”压缩包内的 Induction.v 文件中为您提供，但它未包含在输出 Induction.html 中，可能是由于.v 文件中存在拼写错误。相关代码，这将是“命名案例”部分的第二段(紧接在“……但更好的方法是使用 Case 策略”之后，以及紧接在“Here's an example of how使用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.

(旁注:当我学习 Software Foundations 时，我发现使用提供的 .v 文件作为我的工作 Material 非常有帮助。您不必担心删除的代码，您不必重新输入定义，所有问题都在那里。当然，您的情况可能会有所不同。)