在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的开发通常倾向于使用索引归纳类型来编写这样的代码.这是Coq分布中的矢量库所遵循的解决方案.在那里,你将定义(称为索引感应式的载体,另一个用于有界整数Vector.t和Fin.t分别在标准库).有些函数,例如nth,以这种方式编写起来要简单得多,因为对于向量和索引的模式匹配,最终会在摆脱矛盾的情况并进行递归调用时为你做一些推理.缺点是Coq中的依赖模式匹配不是很直观,有时您必须以奇怪的方式编写函数才能使它们起作用.这种方法的另一个问题是需要重新定义许多在列表上工作的函数来处理向量.

另一个解决方案是将有界整数定义为a的依赖对,nat并证明该索引是有界的,这基本上就是你提到{ | }类型时的目的.这是ssreflect库所遵循的方法,例如(查看ordinal类型).要定义一个安全的nth函数,他们所做的是定义一个简单的版本,它在索引超出范围时使用默认元素返回,并使用n < length l提供该默认元素的证明(例如在元组库中查看)ssreflect,它们定义长度索引列表,并查看它们如何定义tnth).优点是更容易将更多信息类型和功能与更简单的变体相关联.缺点是有些东西变得难以直接表达:例如,你不能直接在ssreflect元组上进行模式匹配.

值得注意的另一点是,通常使用布尔属性而不是归纳定义的更容易,因为计算和简化消除了对某些引理的需要.因此,使用的布尔版本时<,勒柯克不作的证据之间的差异0 < 0 = true和false = true,或证明与S n < length (x :: l) = true和的证明n < length l = true,这意味着你将能够直接在您的定义中使用的证明nth,而无需用辅助外le按摩它们.遗憾的是,Coq标准库倾向于优先于布尔计算的归纳定义类型,在许多情况下它们是无用的,例如用于定义<.该ssreflect库,而另一方面,使定义特性,使得其更适合这种编程风格更使用布尔计算.