1

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

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

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

4

1 回答 1

1

您在分支上看到的函数术语是您rectEuc如何告诉 Coq 模式匹配分支是矛盾的。例如，在您的第一个递归函数中，您用它来表示第一个v'不能是 cons，因为它的长度为零。您在最后一个分支中收到错误的原因是因为这种情况并不矛盾：您的函数类型中没有任何东西可以防止这种情况 k = 0和n = 0.

要在索引族上编写依赖类型的程序，您通常需要使用convoy 模式x：为了在某个表达式上分支后细化参数的类型，您match需要返回一个抽象 over 的函数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 中以这种风格进行编程，因为这样会使得编写程序和以后理解它们变得困难。通常最好编写一个没有依赖类型的程序，并在事后证明它具有您关心的某些属性。（例如，尝试证明使用向量反转列表两次会产生相同的列表！）当然，在某些情况下依赖类型很有用，但大多数时候不需要它们。

于 2020-09-18T13:52:02.473 回答