Coq/Proof General中的Agda编程？

Question

与Agda不同,Coq倾向于将证明与功能分开.Coq提供的策略非常适合编写校样,但我想知道是否有办法复制一些Agda模式功能.

具体来说,我想:

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

这是可能的,在CoqIde或Proof General中？

Answer 1

正如ejgallego在评论中所建议的,你可以(几乎)做到这一点.有一个company-coq工具,它在ProofGeneral之上工作.

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

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

输入refine ().,然后将光标放在parens中并键入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,它有助于将当前目标提取到单独的引理/辅助函数中.

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"计算方式"的类型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阿格达的类比是......

  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的有趣的小编程语言.