Coq依赖类型

Question

我是Coq新手，需要一些帮助，以帮助一些简单的示例让我开始。具体而言，我有兴趣使用依赖类型来定义向量的一些操作（固定大小列表）。我从Vector包开始尝试实现一些附加功能。例如，我很难实现简单的'take'和'drop'函数，这些函数会从列表中删除第一个'p'元素。

Require Import Vector. 

Fixpoint take {A} {n} (p:nat) (a: t A n) : p<=n -> t A p := 
    match a return (p<=n -> t A p) with 
    | cons A v (S m) => cons (hd v) (take m (tl v)) m 
    | nil => fun pf => a 
    end. 

（在nil情况下）的错误是：

The term "a" has type "t A n" while it is expected to have type "t A p". 

有人能帮助我做一些出发点？谢谢！

Answer 1

我不明白你的方法。当参数是非空向量时，您总是返回一个非空向量，但take必须返回nil，而不管向量是否为p=0。

以下是建立take的一种方法。我没有使用假设p <= n，而是将参数n的长度表示为要采用的元素的数量与尾部元素的数量m的总和，其可能是如果p <= n。这允许更容易的递归定义，因为(S p') + m在结构上等于S (p' + m)。请注意，区分度取决于要采用的元素数量：如果采用0返回nil，否则返回cons head new_tail。

该版本的take函数具有所需的计算行为，所以剩下的就是定义一个具有所需证明内容的函数。我使用Program功能来方便地执行此操作：填写计算内容（微不足道，我只需要说我想用m = n - p），然后完成证明义务（这是简单的算术）。

Require Import Arith. 
Require Import Vector. 

Fixpoint take_plus {A} {m} (p:nat) : t A (p+m) -> t A p := 
    match p return t A (p+m) -> t A p with 
    | 0 => fun a => nil _ 
    | S p' => fun a => cons A (hd a) _ (take_plus p' (tl a)) 
    end. 
Program Definition take A n p (a : t A n) (H : p <= n) : t A p := 
      take_plus (m := n - p) p a. 
Solve Obligations using auto with arith. 

---

为了您newdrop : forall A n p, t A n -> p <= n -> t A (n-p)，下面的方法工作。你需要通过告诉它什么p和n成为递归调用来帮助Coq。

Program Fixpoint newdrop {A} {n} p : t A n -> p <= n -> t A (n-p) := 
    match p return t A n -> p <= n -> t A (n-p) with 
    | 0 => fun a H => a 
    | S p' => fun a H => newdrop p' (tl a) (_ : p' <= n - 1) 
    end. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 
Next Obligation. 
omega. 
Qed. 

我不知道为什么Solve Obligations using omega.不工作，但每解决个别的义务工作。