coq - 在 coq 中编写隐式证明对象的不可能模式

Question

我试图将 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 中执行此操作？

Answer 1

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

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 channel 中提出的 gdsfhl 作为解决方案:

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

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