linux - 如何在 linux 中为 Coq 代码使用交互式 shell？

Question

我想在 Coq 中编写和调试代码，类似于我在 Python、R 等中编写代码的方式。具体来说:

我有一个终端窗口，我的 code.v显示文件，例如:

Definition double (x:nat) : nat := 2 * x.
Definition tripple (x:nat) : nat := 3 * x.

现在在另一个终端中，我想要一个可以接受命令的交互式 shell从 code.v 加载代码，检查它等。例如:

Load code.v // What's the command for this?
Print double. // Expect to see output "double : nat -> nat"

问题 1:什么样的命令为我提供了这样的交互式 shell，我应该在交互式 shell 中执行什么命令来加载文件？

此外，如果在我的code.v文件我有一个未完成的证明，例如

Lemma ex4: forall (X : Set) (P : X -> Prop),
  ~(forall x, ~ (P x)) -> (exists x, (P x)).
Proof.
  intros X P A.
  apply not_all_ex_not in A.
  destruct A.

问题 2: 是否有来自交互式 shell 的命令，如 check code.v这会打印出我的证明状态，就像 Coqide 在您按 ctrl+down 时所做的那样

1 subgoal
X : Set
P : X -> Prop
x : X
H : ~ ~ P x
______________________________________(1/1)
exists x0 : X, P x0

请注意，我更喜欢通过 linux 终端来做所有事情，而不是使用 IDE。

Answer 1

通常，如果您通过通常的方式安装了 coq 和 coqide，您应该有一个名为 coqtop 的命令(它是 coq toplevel 的简写).它从 stdin 读取所有命令并在 stdout 中打印所有结果(通常会进入 coqide 的目标或响应窗口)。

使用您的 code.v 示例，您可以运行以下命令。

coqtop -require-import Classical < code.v

这将显示文件中所有命令生成的所有输出并终止。最后一个输出将是最后一个命令的结果，这样就可以看到最后一个打开的目标。请注意，-require-import Classical 是必需的，因为在该模块中定义了引理 not_all_ex_not。

实际上，这不是很方便，因为每次添加新命令时都必须重新运行整个文件。您还可以通过键入以下命令行来保持系统运行，并执行已记录的文件 code.v。

coqtop -require-import Classical -load-vernac-source code.v

这不会显示最后一个命令后的目标，但您可以通过键入命令 Show 来要求它。 然后您可以在终端中键入更多命令以查看它们对状态的影响coqtop 程序。然后，您有责任记录您发送到 coqtop 的命令，以便稍后复制证明。 coqide、proof-general 或 vscoq 等用户界面主要用于帮助您完成此录制任务。

要了解更多信息，您应该输入

coqtop --help

您还应该考虑将 coqtop 与 rlwrap 结合使用。