types - Coq 程序配对

Question

我试图使用子集类型为列表执行安全的 get 函数。我使用程序尝试了这个定义

Program Fixpoint get A (l : list A) (n : {x : nat | x < length l} ) : A :=
  match (n, l) with
  | (O, x :: l') => x
  | (S n', x :: l') => get l' n'
  | _ => _
  end.

问题是它出现以下错误

找到归纳类型 nat 的构造函数，同时发现 sig 的构造函数
预计。

为什么 coq 不允许我对包含子集类型的模式进行匹配？

Answer 1

问题在于，Coq 中多个值的模式匹配形式很特殊。你需要这样写:

Program Fixpoint get A (l : list A) (n : {x : nat | x < length l} ) : A :=
  match n, l with
  | O, x :: l' => x
  | S n', x :: l' => get _ l' n'
  | _, _ => _
  end.

在之前的版本中，您实际上是对 (n, l) 对进行模式匹配，而不是对值 n 和 l 进行模式匹配 同时，Program 可能因此而感到困惑。