Coq/Proof General中是否支持类似Agda的编程方式？

Question

与Agda不同，Coq倾向于将证明与函数分开。Coq提供的策略非常适合编写证明，但我想知道是否有一种方法可以复制一些Agda-mode的功能。

具体来说，我想要：

• 一些类似于Agda的 ? 或 Haskell 的 _，在编写函数时可以省略部分内容，然后（希望）让Coq告诉我需要放置在那里的类型
• 相当于Agda mode中的C-c C-r(reify)的功能，在 ? 块中填充一个函数，它将为所需参数创建新的 ? 块
• 当我在函数中进行匹配时，Coq自动扩展出可能的分支（例如Agda-mode中的C-c C-a）

这在CoqIde或Proof General中是否可行？

- jmite

---

您可以做其中的一部分，但不能以完全相同的方式进行。第一点，您可以使用refine（请参阅文档）。第二个要点可能会更困难，因为我认为当前的Coq IDE还无法使用类型信息，我猜想company-coq可能有助于第三个要点。 - ejgallego

@ejgallego 公司 Coq 是为您创建所有分支（即用 LHS 上的模式填充）还是只添加一个分支并让您填写两侧？ - jmite

在CoqIDE中，有一个创建匹配的快捷键（默认为“ctrl + shift + m”）。您必须先将光标放置或选择正确的类型。 - eponier

对于 match，你的意思是按 C-c C-c 键，对吗？ - pigworker

Answer 1

正如ejgallego在评论中建议的那样，你可以（几乎）做到。有一个名为company-coq的工具，它在ProofGeneral之上运行。

让我演示一下如何使用company-coq和refine策略来实现map函数。从以下代码开始：

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.

在输入refine ().后，将光标放在括号内并键入C-c C-a RET list RET -- 它会在带有需要手动填写的空缺的列表上插入一个match表达式（让我们填写列表名称和基本情况）。

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x x0 => cons _ _
          end).

为了完成这个任务，我们将x0重命名为tl，并提供递归情况exact (map A B f tl).，其中内容涉及编程。请注意，需要保留HTML标签。

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x tl => cons _ _
          end).
  exact (f x).
  exact (map A B f tl).
Defined.

还有一个有用的键盘快捷键C-c C-a C-x，可帮助将当前目标提取到单独的引理/辅助函数中。

- Anton Trunov

---

非常酷！所以，我错过的重要一点是，您可以使用像“refine”和“exact”这样的策略来定义Fixpoints，以及证明。 - jmite

根据Curry-Howard对应理论，不应该有任何区别 :) 策略是用于构建项的语言。只需以“Defined”而非“Qed”结束与计算相关的定义，否则Coq会认为该定义是不透明的，无法展开它。 - Anton Trunov

主要问题在于，company-coq对洞的支持有些脆弱，因为它大多数情况下使用正则表达式与Coq进行通信。希望未来可以使用更结构化的协议（如Agda）。 - ejgallego

看起来 apply 策略在 Agda 中与 Reify 相当接近。 - jmite

Answer 2

让我教你一个奇怪的技巧。它可能不是解决你所有问题的答案，但至少在概念上可以帮助你。

让我们为自然数实现加法，后者由以下方式给出：

Inductive nat : Set :=
  | zero : nat
  | suc : nat -> nat.

你可以尝试通过策略来写加法，但这种情况会发生。

Theorem plus' : nat -> nat -> nat.
Proof.
  induction 1.

plus' < 2 subgoals

  ============================
   nat -> nat

subgoal 2 is:
 nat -> nat

你看不清自己在做什么。

关键是要更仔细地观察你正在做的事情。我们可以引入一个毫无必要的依赖类型，克隆nat。

Inductive PLUS (x y : nat) : Set :=
  | defPLUS : nat -> PLUS x y.

这里的想法是，PLUS x y 表示 "计算 x + y 的方法"。我们需要一个投影函数，可以提取这种计算的结果。

Theorem usePLUS : forall x y, PLUS x y -> nat.
Proof.
  induction 1.
    exact n.
Defined.

现在我们已经准备好通过提供程序来编程。

Theorem mkPLUS : forall x y, PLUS x y.
Proof.

mkPLUS < 1 subgoal

  ============================
   forall x y : nat, PLUS x y

目标的结论向我们展示了当前的左侧和上下文。在Agda中，C-c C-c的类比是...

  induction x.

mkPLUS < 2 subgoals

  ============================
   forall y : nat, PLUS zero y

subgoal 2 is:
 forall y : nat, PLUS (suc x) y

你可以看到它已经进行了案例分割！让我们去掉基本情况。

    intros y.
      exact (defPLUS zero y    y).

调用PLUS的构造函数就像写一个方程式。想象在它的第三个参数前有一个=符号。对于步进情况，我们需要进行递归调用。

    intros y.
      eapply (fun h => (defPLUS (suc x) y    (suc (usePLUS x y h)))).

为了进行递归调用，我们使用所需参数调用 usePLUS，这里是 x 和 y，但我们对第三个参数进行抽象，即如何实际计算它的说明。最终目标只剩下这个子目标，实质上是终止检查。

mkPLUS < 1 subgoal

  x : nat
  IHx : forall y : nat, PLUS x y
  y : nat
  ============================
   PLUS x y

现在，您不再使用Coq的守卫检查，而是使用...

        auto.

…这检查归纳假设覆盖递归调用。我们正在

该段文本是关于计算机科学中的递归程序设计方面的内容，其中提到了一种方法来检查归纳假设是否覆盖了递归调用。

Defined.

我们有一个工作者，但我们需要一个包装器。

Theorem plus : nat -> nat -> nat.
Proof.
  intros x y.
    exact (usePLUS x y (mkPLUS x y)).
Defined.

我们准备好了。

Eval compute in (plus (suc (suc zero)) (suc (suc zero))).

Coq <      = suc (suc (suc (suc zero)))
     : nat

您拥有一个交互式的构建工具。通过使类型更加详细，您可以将其优化以显示解决问题所需的相关细节。生成的证明脚本...

Theorem mkPLUS : forall x y, PLUS x y.
Proof.
  induction x.
    intros y.
      exact             (defPLUS zero    y    y).
    intros y.
      eapply (fun h =>  (defPLUS (suc x) y    (suc (usePLUS x y h)))).
        auto.
Defined.

...明确指出了它构建的程序。你可以看到它定义了加法。

如果你自动化这个程序构建过程，并添加一个界面来显示你正在构建的程序和关键的问题简化策略，那么你就得到了一个有趣的小型编程语言，叫做Epigram 1。

- pigworker