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.不工作，但每解決個別的義務工作。