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

我正在努力学习Coq,但我发现很难从我在软件基础和依赖类型认证编程中读到的内容跳到我自己的用例.

特别是,我想我会尝试在列表上制作第n个函数的验证版本.我设法写了这个：

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.

这有效,但它提出了两个问题：

>经验丰富的Coq用户如何写这个？这三个引理真的有必要吗？这是{|的用例吗？类型？
>如何从其他代码调用此函数,即如何提供所需的校样？

我试过这个：

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

但是,当我弄明白要写什么之后,这当然不会奏效.部分.我尝试在那里放置(2<长度[1; 2; 3]),但是它具有类型Prop而不是类型2<长度[1; 2; 3].我可以编写并证明该特定类型的引理,并且有效.但是什么是一般解决方案？

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,你会得到更整洁的代码.