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

Question

我正在尝试学习 Coq，但我发现很难从 Software Foundations 和 Certified Programming with Dependent Types 中阅读的内容飞跃到我自己的用例。

特别是，我想我会尝试在列表中创建 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 开发倾向于支持索引归纳类型来编写这样的代码。这是 Coq 发行版中 vector library 所遵循的解决方案。在那里，您将为向量定义一个索引归纳类型，为有界整数定义另一种（在标准库中分别称为Vector.t 和Fin.t）。一些函数，比如nth，用这种风格写起来要简单得多，因为向量和索引上的模式匹配最终会在消除矛盾的情况和进行递归调用时为你做一些推理。缺点是 Coq 中的依赖模式匹配不是很直观，有时你必须以一种奇怪的方式编写函数才能让它们工作。这种方法的另一个问题是，需要重新定义许多作用于列表的函数以作用于向量。

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

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

Answer 2

zltz 与nltz 0 具有相同的类型。

Check zltz.
Check nltz 0.

要将您的函数与另一个函数中的2 和[1; 2; 3] 一起使用，您可以使用lt_dec。

Eval compute in match lt_dec 2 (length [1; 2; 3]) with
  | left pf => safe_nth 2 [1; 2; 3] pf
  | right _ => 0
  end.

如果你提取lt_dec，你会发现它与删除证明后的ltb非常相似。如果您可以从调用 safe_nth 的函数中构建证明，则无需使用 lt_dec。

你可以像这样缩短你的函数。

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

我不确定最佳实践是什么，但如果您使用 sig，您会得到更整洁的提取代码。