如何在 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： 是否有来自像 check code.v 这样的交互式 shell 的命令可以打印出我的证明状态，就像 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 顶层的简写）。它从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 结合使用。