Coq 程序配对

Question

我试图为使用子集类型的列表做一个安全的 get 函数。我使用 program

尝试了这个定义

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.

问题是出现以下错误

Found a constructor of inductive type nat while a constructor of sig is expected.

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

Answer 1

您有一个 sig 并且您正试图获得一个国家。 sig 是 nat with 证明的证人：https://coq.inria.fr/library/Coq.Init.Specif.html。您需要匹配 proj1_sig n，这将解压号码。您真的可以将符号 {x | P x} 视为一个元组（从技术上讲，它是一个从属和）：

Notation "{ x | P }" := (sig (fun x => P)) : type_scope.

因此，每当您看到 { x | P } 时，您都会将其视为 (x,P)。问题是您期望 n 类型不同。

Answer 2

问题是多值模式匹配的形式在 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 大概是因为这个而感到困惑吧。

Coq 程序配对

Coq Program matching on pair

types

subset

coq