coq - 在 Coq 中使用依赖类型(安全第 n 个函数)

Question

我正在尝试学习 Coq，但我发现很难从我在《软件基础》和《依赖类型认证编程》中读到的内容过渡到我自己的内容用例。

特别是，我想尝试制作 nth 的验证版本列表上的函数。我设法写了这个:

Require Import Arith.
Require Import List.
Import ListNotations.

Lemma zltz: 0 < 0 -> False.
Proof.
  intros. contradict H. apply Lt.lt_irrefl.
Qed.

Lemma nltz: forall n: nat, n < 0 -> False.
Proof.
  intros. contradict H. apply Lt.lt_n_0.
Qed.

Lemma predecessor_proof: forall {X: Type} (n: nat) (x: X) (xs: list X),
  S n < length (x::xs) -> n < length xs.
Proof.
  intros. simpl in H. apply Lt.lt_S_n. assumption.
Qed.

Fixpoint safe_nth {X: Type} (n: nat) (xs: list X): n < length xs -> X :=
  match n, xs with
  | 0, [] => fun pf: 0 < length [] => match zltz pf with end
  | S n', [] => fun pf: S n' < length [] => match nltz (S n') pf with end
  | 0, x::_ => fun _ => x
  | S n', x::xs' => fun pf: S n' < length (x::xs') => safe_nth n' xs' (predecessor_proof n' x xs' pf)
  end.

这可行，但它提出了两个问题:

1. 经验丰富的 Coq 用户会如何写这个？这三个引理真的有必要吗？这是 { | } 的用例吗？类型？
2. 如何从其他代码中调用此函数，即如何提供所需的证明？

我尝试过这个:

Require Import NPeano.
Eval compute in if ltb 2 (length [1; 2; 3]) then safe_nth 2 [1; 2; 3] ??? else 0.

但是当然，除非我弄清楚要为 ??? 写什么，否则这不会起作用。部分。我尝试输入 (2 < length [1; 2; 3])但有类型 Prop而不是输入 2 < length [1; 2; 3] 。我可以编写并证明该特定类型的引理，并且这是有效的。但一般的解决方案是什么？

Answer 1

我认为对于做这类事情的最佳方法是什么没有达成共识。

我相信 Coq 开发通常倾向于使用索引归纳类型来编写这样的代码。这是 vector library 后面的解决方案在 Coq 发行版中。在那里，您可以为向量定义一种索引归纳类型，为有界整数定义另一种索引归纳类型(在标准库中分别称为 Vector.t 和 Fin.t)。一些函数，如nth ，用这种风格编写要简单得多，因为例如，在消除矛盾的情况和进行递归调用时，向量和索引上的模式匹配最终会为您进行一些推理。缺点是 Coq 中的依赖模式匹配不是很直观，有时你必须以奇怪的方式编写函数才能让它们工作。这种方法的另一个问题是，需要重新定义许多适用于列表的函数才能适用于向量。

另一个解决方案是将有界整数定义为 nat 的依赖对。以及该索引有界的证明，这本质上就是您提到 { | } 时所追求的。类型。这是 ssreflect 遵循的方法。例如，库(查找 ordinal 类型)。定义一个安全nth函数，他们所做的就是定义一个简单的版本，当索引越界时返回一个默认元素，并使用 n < length l 的证明提供该默认元素(例如查看 ssreflect 的 tuple 库，它们在其中定义长度索引列表，并了解它们如何定义 tnth )。优点是更容易将信息更丰富的类型和函数与更简单的变体联系起来。缺点是有些事情变得更难以直接表达:例如，您无法直接对 ssreflect 元组进行模式匹配。

值得注意的另一点是，通常使用 bool 属性比归纳定义的属性更容易，因为计算和简化消除了对某些引理的需要。因此，当使用 < 的 bool 版本时，Coq 不会区分 0 < 0 = true 的证明和false = true ，或 S n < length (x :: l) = true 的证明之间以及 n < length l = true 的证明，这意味着您可以直接在 nth 的定义中使用这些证明无需用辅助引理来按摩它们。不幸的是，Coq 标准库在许多情况下倾向于使用归纳定义的类型而不是 bool 计算，而 bool 计算在这些情况下并没有什么用处，例如定义 < 。 ssreflect另一方面，库更多地使用 bool 计算来定义属性，使其更适合这种编程风格。