尝试使用Case时出现coq错误。 Software Foundations书中的示例 [英] coq error when trying to use Case. Example from Software Foundations book

问题描述

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

I am trying to learn Coq by working through the online Software Foundations book: http://www.cis.upenn.edu/~bcpierce/sf/

我正在使用交互式命令行Coq解释器 coqtop 。

I'm using the interactive command line Coq interpreter coqtop.

在归纳章节中（ http://www.cis.upenn.edu/~bcpierce/sf/Induction.html ），我正在严格按照说明进行操作。我使用 coqc Basics.v 编译Basics.v。然后，我启动 coqtop 并精确键入：

In the induction chapter (http://www.cis.upenn.edu/~bcpierce/sf/Induction.html), I am following the instructions exactly. I compile Basics.v using coqc Basics.v. I then start coqtop and type exactly:

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

一切正常，直到最后一行，这时我得到以下错误：

Everything works until that last line, at which point I get the following error:

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

对于Coq来说我太陌生了，无法开始整理为什么它行不通。我在网上发现了一些东西，提示我需要执行 Require String。，但是，这也不起作用。有没有人读过本书或遇到这个问题？如何使代码正常工作？

I'm too new to Coq to start to unpack why this isn't working. I found something online suggesting I needed to do Require String. first, however, this didn't work either. Has anyone worked through this book or encountered this problem? How do I get the code to work properly?

这个Case关键字（策略？）似乎依赖于SF书没有明确说明的其他内容，但我不知道要做什么。 / p>

This Case keyword (tactic?) seems to be dependent on something else that the SF book is not making clear is needed, but I can't figure out what.

推荐答案

缺少的是一个字符串数据类型，该数据类型挂接到 ... 符号； String 模块包含这样的表示法和数据类型，但是您必须告诉Coq通过 Open Scope string_scope使用该表示法。但是，还缺少 Case 的实现，该实现仅在解决字符串问题后才会显示。所有这些都是在下载压缩包中的 Induction.v 文件中提供的，但未包含在输出 Induction.html中，可能是由于 .v 文件中的错字所致。相关代码将是命名案例部分的第二段（紧接在…但更好的方法是使用 Case 策略之后） 这是一个使用 Case 的例子……）是：

What's missing is a string datatype which hooks into the "..." notation; the String module contains such a notation and datatype, but you have to tell Coq to use that notation via Open Scope string_scope. What's also missing, however, is an implementation of Case, which will only show up after you fix the string problem. All of this is provided for you in the Induction.v file inside the "Download" tarball, but it is not included in the output Induction.html, possibly due to a typo in the .v file. The relevant code, which would be the second paragraph of the "Naming Cases" section (right after "…but a better way is to use the Case tactic," and right before "Here's an example of how Case is used…") is:

(* [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 文件作为我的工作资料非常有帮助，您不必担心代码被删除，不必重新输入定义，所有问题都在那里。当然，您的里程可能会有所不同。）

(A side note: When I worked through Software Foundations, I found using the provided .v files as my work material to be very helpful. You don't have to worry about elided code, you don't have to retype the definitions, and all the problems are right there. Your mileage may vary, of course.)

这篇关于尝试使用Case时出现coq错误。 Software Foundations书中的示例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！