3

我试图将 coq 用作具有依赖类型的编程语言。我创建了以下小程序：

Inductive Good : list nat -> Set := 
  | GoodNonEmpty : forall h t, Good (h :: t).

Definition get_first(l : list nat)(good : Good l) : nat := 
  match l with
    | h :: t => h
    | nil => 
      match good with 
      end
  end.

我为非空列表定义了一个类型，并创建了一个函数，该函数获取此类列表的第一个元素，前提是有证据证明它不为空。我很好地处理了头项目由两个项目组成的情况，但我无法处理空列表的不可能情况。我怎样才能在 coq 中做到这一点？

4

1 回答 1

6

一种比您尝试更简单的方法是：

Definition get_first (l : list nat) (good : Good l) : nat :=
  match good with
  | GoodNonEmpty h _ => h
  end.

这是一种按照您想要的方式进行操作的方法。你会注意到证明“Good nil”不存在是非常冗长的，内联。

Definition get_first (l : list nat) (good : Good l) : nat :=
  (
    match l as l' return (Good l' -> nat) with
    | nil =>
      fun (goodnil : Good nil) =>
        (
          match goodnil in (Good l'') return (nil = l'' -> nat) with
          | GoodNonEmpty h t =>
            fun H => False_rect _ (nil_cons H)
          end
        )
        (@eq_refl _ nil)
    | h :: _ => fun _ => h
    end
  ) good.

您当然可以在外部定义一些内容并重用它。不过，我不知道最佳实践。也许有人可以用更短的方法来做同样的事情。

编辑：

顺便说一句，您可以在证明模式下以更简单的方式获得几乎相同的结果：

Definition get_first' (l : list nat) (good : Good l) : nat.
Proof.
  destruct l. inversion good. exact n.
Defined.

然后您可以：

Print get_first'.

看看 Coq 是如何定义它的。但是，对于更多涉及的事情，您最好遵循 #coq IRC 频道中提出的 gdsfhl 作为解决方案：

http://paste.in.ua/4782/

您可以看到他使用该refine策略来提供术语的部分骨架来编写，并推迟缺少的证明。

于 2012-09-22T18:48:35.163 回答