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.

问题是它得到以下错误

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

为什么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也可能因此而感到困惑.