我正在尝试通过在线软件基础书籍来学习 Coq:http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/
我正在使用交互式命令行 Coq 解释器coqtop
.
在归纳章节中(http://www.cis.upenn.edu/~bcpierce/sf/Induction.html http://www.cis.upenn.edu/~bcpierce/sf/Induction.html),我完全按照说明进行操作。我使用编译 Basics.vcoqc 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 书没有明确说明的其他东西,但我不知道是什么。
缺少的是一个字符串数据类型,它挂接到"..."
符号;这String
模块包含这样的符号和数据类型,但是你必须告诉 Coq 通过以下方式使用该符号Open Scope string_scope.
然而,还缺少的是Case
,只有在修复字符串问题后才会显示。所有这些都在Induction.v
文件位于“下载”压缩包内,但不包含在输出中Induction.html
,可能是由于拼写错误.v
文件。相关代码,这将是“命名案例”部分的第二段(就在“...但更好的方法是使用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
文件作为我的工作材料非常有帮助。您不必担心省略的代码,不必重新输入定义,所有问题都在那里。当然,您的里程可能会有所不同。)
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)