Vector error : The type of this term is a product

Question

我想要向量的最后 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:=[]}).

问题出在代码底部的第二行。

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

Answer 1

你在 rectEuc 的分支上看到的函数项是你如何告诉 Coq pattern-match 分支是矛盾的。例如，在你的第一个递归函数中，你用它来表示第一个 v' 不能是缺点，因为它的长度为零。您在最后一个分支中收到错误的原因是因为这种情况不自相矛盾：函数类型中没有任何内容可以阻止 k = 0 和 n = 0 的情况.

要在索引族上编写依赖类型的程序，您通常需要使用 convoy 模式：在对某些表达式进行分支后细化参数的类型 x ，您的 match 需要 return 一个对 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函数来指定结果的长度：结果不能大于原始向量！

Fixpoint but_last n : Euc (S n) -> Euc n :=
  match n with
  | 0   => fun _ => []
  | S n => fun v => head _ v ::: but_last n (tail _ v)
  end.

Fixpoint snoc n (v : Euc n) (x : R) : Euc (S n) :=
  match v with
  | [] => [x]
  | y ::: v => y ::: snoc _ v x
  end.

Fixpoint lastk k : forall n, Euc n -> Euc (Nat.min k n) :=
  match k with
  | 0 => fun _ _ => []
  | S k => fun n =>
    match n return Euc n -> Euc (Nat.min (S k) n) with
    | 0 => fun _ => []
    | S n => fun v =>
      snoc _ (lastk k _ (but_last _ v)) (last _ v)
    end
  end.

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

Vector error : The type of this term is a product

Vector error : The type of this term is a product

coq

dependent-type

convoy-pattern