类似Agda的Coq/编程？

Question

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

具体来说，我想：

• 类似于Agda的?或Haskell的_，在编写函数时我可以省略它的一部分，并且(希望) Coq告诉我需要放在那里的类型
• 相当于Agda模式下的C- C -r (reify)，在这里您用函数填充?块，它将为所需的参数生成新的?块。
• 当我在一个函数中执行match时，让Coq自动写出可能的分支(比如在Agda模式下的Coq)

这是可能的，在CoqIde还是证据一般？

Answer 1

让我教你一个诡计。这可能不是你所有担忧的答案，但至少在概念上可能会有所帮助。

让我们实现自然数的加法，后者由

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是“计算plus 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

这个目标的结论向我们展示了我们目前的左手边和背景.C-c C-c在Agda中的类似物是。

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

调用加号的构造函数就像编写方程一样。想象一下在第三个论点之前有一个=符号。对于步骤情况，我们需要进行递归调用。

    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.

...which检查归纳假设是否包括递归调用。我们是

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.

...is显式地说明它构造的程序。你可以看到这是定义加法。

如果您自动化这个程序构建设置，然后在一个界面上显示您正在构建的程序和关键问题-简化策略，您会得到一个有趣的小编程语言，叫做Epigram 1。