在 Coq 中使用依赖类型（安全第 n 个函数）

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

特别是，我想我应该尝试制作一个经过验证的版本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 用户会如何写这个？这三个引理真的有必要吗？这是一个用例吗{ | } types?
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]。我可以编写并证明该特定类型的引理，并且这是有效的。但一般的解决方案是什么？

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

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

另一个解决方案是将有界整数定义为 a 的依赖对nat以及该索引是有界的证明，这本质上就是您提到的时候想要的{ | }类型。这是以下方法所遵循的ss反射 http://ssr.msr-inria.inria.fr/~jenkins/current/Ssreflect.fintype.html例如，图书馆（寻找ordinal类型）。定义一个安全的nth函数，他们所做的是定义一个简单的版本，当索引越界时返回一个默认元素，并使用以下证明：n < length l提供默认元素（例如看看tuple http://ssr.msr-inria.inria.fr/~jenkins/current/Ssreflect.tuple.htmlssreflect 库，他们在其中定义长度索引列表，并了解它们如何定义tnth）。优点是更容易将信息更丰富的类型和函数与更简单的变体联系起来。缺点是有些事情变得更难以直接表达：例如，您不能直接在 ssreflect 元组上进行模式匹配。

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