向量错误：此术语的类型是产品

如何解决向量错误：此术语的类型是产品

我想要向量的最后k个元素。我是参考Coq.Vectors.VectorDef编写此代码的。

 Require Import Coq.Reals.Reals.

 (* vector of R *)
 Inductive Euc:nat -> Type:=
 |RO : Euc 0
 |Rn : forall {n:nat},R -> Euc n -> Euc (S n).

 Notation "[ ]" := RO.
 Notation "[ r1,..,r2 ]" := (Rn r1 .. ( Rn r2 RO ) .. ).
 Infix ":::" := Rn (at level 60,right associativity).

 (* return length of vector *)
 Definition EucLength {n}(e:Euc n) :nat:= n.

 Definition rectEuc (P:forall {n},Euc (S n) -> Type)
 (bas: forall a:R,P [a])
 (rect: forall {n} a (v: Euc (S n)),P v -> P (a ::: v)) :=
 fix rectEuc_fix {n} (v: Euc (S n)) : P v :=
 match v with
 |@Rn 0 a v' =>
   match v' with
     |RO => bas a
     |_ => fun devil => False_ind (@IDProp) devil
   end
 |@Rn (S nn') a v' => rect a v' (rectEuc_fix v')
 |_ => fun devil => False_ind (@IDProp) devil
 end.

 (* eliminate last element from vector *)
 Definition EucElimLast := @rectEuc (fun n _ => Euc n) (fun a => []) (fun _ a _ H => a ::: H).

 (* this function has an error *)
 Definition rectEucLastN (P:forall {n},nat -> Euc n -> Type)
 (bas: forall {n} k (e:Euc n),P k e)
 (rect: forall {n} k a (e:Euc (S n)),P k e -> P (S k) (a ::: e)) :=
 fix rectEuc_fix {n} (k:nat) (e:Euc n): P k e :=
 match k,e with
 |S k',e' ::: es => rect k' e' (rectEuc_fix k' (EucElimLast ((EucLength e)-1) e))
 |0%nat,e' ::: es => bas k e
 |_,_ => fun devil => False_ind (@IDProp) devil
 end.

rectEucLastN说The type of this term is a product while it is expected to be (P ?n@{n1:=0%nat} ?n0@{k1:=0%nat} ?e@{n1:=0%nat; e1:=[]}).

问题是代码底部的第二行。

为什么最后一个模式有错误？

解决方法

您在rectEuc分支上看到的函数项是如何告诉Coq模式匹配分支是矛盾的。例如，在第一个递归函数中，您用它来表示第一个v'不能是一个缺点，因为它的长度为零。在上一个分支中出现错误的原因是该情况与不是矛盾的：函数类型中的任何内容都不能阻止情况k = 0和n = 0。>

要在索引族中编写依赖类型的程序，通常需要使用 convoy模式：在某些表达式上分支后，精炼参数x的类型，您的{{1 }}需要返回一个在match上抽象的函数。例如，此函数通过在向量的长度上递归来计算向量的最后一个元素。在x分支中，我们需要知道S的长度以某种方式连接到v。

n

这是提取最后Definition head n (v : Euc (S n)) : R := match v with | x ::: _ => x end. Definition tail n (v : Euc (S n)) : Euc n := match v with | _ ::: v => v end. Fixpoint last n : Euc (S n) -> R := match n with | 0 => fun v => head 0 v | S n => fun v => last n (tail _ v) end. 个元素的代码。请注意，其类型使用k函数指定结果的长度：结果不能大于原始向量！

Nat.min

就个人而言，我建议您不要在Coq中使用这种样式的编程，因为这样做会使以后编写程序和理解它们变得困难。通常最好编写一个没有依赖类型的程序，并在事实中证明它具有您关心的某些特性后再进行验证。 （例如，尝试显示使用向量将列表反转两次会产生相同的列表！）当然，在某些情况下，依赖类型是有用的，但大多数时候不需要它们。