10

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

具体来说，我想：

  • 相当于 Agda?或 Haskell 的_，我可以在编写函数时省略部分函数，​​并且（希望）让 Coq 告诉我需要放在那里的类型
  • 相当于 Agda 模式 (reify) 中的 Cc Cr，您可以在其中?使用函数填充块，它会?为所需的参数创建新块
  • 当我match在一个函数中执行一个函数时，让 Coq 自动编写扩展可能的分支（如 Agda 模式中的 Cc Ca）

在 CoqIde 或 Proof General 中这可能吗？

4

2 回答 2

6

正如 ejgallego 在评论中所建议的那样，您（几乎）可以做到这一点。有company-coq工具，它在 ProofGeneral 之上工作。

让我演示如何使用 company-coq 和策略map来实现该功能。refine从...开始

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

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有助于将当前目标提取到单独的引理/辅助函数中。

于 2017-01-24T20:40:20.417 回答
5

让我教你一个奇怪的技巧。它可能无法解决您所有的担忧，但它可能会有所帮助，至少在概念上是这样。

让我们实现自然数的加法，后者由下式给出

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

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

    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。

于 2017-01-26T10:16:57.033 回答