勒柯克不能看到兩個類型相同

Question

我試圖定義一個向量的轉速功能，它的大小被嵌入它，我無法弄清楚如何定義它的轉速功能。

這是我喜歡的類型定義：

Inductive vect {X : Type} : nat -> Type -> Type 
    := Nil : vect 0 X 
    | Cons : forall n, X -> vect n X -> vect (S n) X 
. 

---

我已經在上面定義了一些有用的功能：

Fixpoint app {X : Type} {n m : nat} (v1 : vect n X) (v2 : vect m X) 
: vect (n + m) X := 
    match v1 with 
    | Nil => v2 
    | Cons _ x xs => Cons _ x (app xs v2) 
    end. 

Fixpoint fold_left {X Y : Type} {n : nat} (f : Y -> X -> Y) (acc : Y) (v : vect n X) 
: Y := 
    match v with 
    | Nil => acc 
    | Cons _ x xs => fold_left f (f acc x) xs 
    end. 

---

而現在，我想定義轉。我的第一個嘗試是通過fold_left，但事實證明這是徹底的失敗。

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := 
    fold_left (fun {X : Type} {k : nat} (acc : vect k X) (x : X) => x ::: acc) {{ }} v. 

我不明白錯誤Error: The type of this term is a product while it is expected to be a sort.。

---

我的第二暫定幾乎是好的，但勒柯克看不到「S N =（N + 1）」本身，我不知道怎麼告訴勒柯克左右。

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := 
    match v in (vect n X) return (vect n X) with 
    | Nil => Nil 
    | Cons _ x xs => app (rev xs) {{ x }} 
    end. 

的誤差爲The term "app (rev X n0 xs) {{x}}" has type "vect (n0 + 1) X" while it is expected to have type "vect (S n0) X"

如果您對COQ代碼的任何其他言論不要猶豫。

Answer 1

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := 
    fold_left (fun {X : Type} {k : nat} (acc : vect k X) (x : X) => Cons x acc) Nil v. 

第一顯式參數fold_left必須有一個類型的形式?1 -> ?2 -> ?1，即兩個參數，其返回類型的功能的相同的第一個參數。 [依賴]「產品」是一個函數的Coq術語。您正在傳遞一個fun (X:Type) b c d => …的表格，因此?1爲Type，並且術語fun c d => …（顯然具有產品類型）必須具有類型?，因此它必須具有類型Type，即它必須是分類。

如果試圖解決這個問題，你會意識到你fold_left功能不能在這裏工作：你需要的迭代過程中改變向量的長度，但迭代器參數fold_left其類型期間常數迭代。使用fold_left函數，如果從累加器Nil（它是一個長度爲0的向量）開始，則最終會得到相同類型的結果，同樣是長度爲0的向量。

我避難所「T想過如何定義，它可以讓你定義rev更一般的迭代器，但我敢肯定，這是可能的。

---

關於你的第二次嘗試，與vect (n0 + 1) X和vect (S n0) X的問題是，它們不是同一類型的，因爲n0 + 1是無法轉換爲S n0。該條款n0 + 1都是平等的，但不能自由兌換，並作爲類型術語僅僅是如果他們兌換互換。

如果兩個類型相同，您可以編寫一個函數，「鑄就」一類的術語成其他類型的術語。實際上，這樣做的一般功能是eq_rect，這是相等類型系列的析構函數。你可能會發現它定義了一個專門的函數來將矢量投射到一個可證明但不一定可變的等長度的矢量上。

Definition vect_eq_nat {X : Type} {m n : nat} (H : m = n) v := 
    eq_rect _ (fun k => @vect X k X) v _ H. 

如果eq_rect使用不會立即站出來，你可以通過戰術定義這樣的功能。只要確定你正在定義一個函數，它不僅具有正確的類型，而且具有所需的結果，並使定義變得透明。

Definition vect_eq_nat {X : Type} {m n : nat} : m = n -> @vect X m X -> @vect X n X. 
intros. 
rewrite <- H. 
exact X0. 
Defined. 
Print vect_eq_nat. 

您還可以使用Program民俗混合證明和條款。

Program Definition vect_plus_comm {X : Type} {n : nat} (v : @vect X (n+1) X) : @vect X (S n) X := 
    vect_eq_nat _ v. 
Require Import Arith. 
Require Import Omega. 
Solve Obligation 0 using (intros; omega). 

現在您可以使用此輔助定義來定義rev。

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := 
    match v in (vect n X) return (vect n X) with 
    | Nil => Nil 
    | Cons _ x xs => vect_plus_comm (app (rev xs) (Cons _ x Nil)) 
    end. 

您可以使用Program Fixpoint直接定義rev，一旦你把那個鑄造到位的一步。一個證明義務是S n0和n0 + 1之間的等同。

Program Fixpoint rev' {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := 
    match v in (vect n X) return (vect n X) with 
    | Nil => Nil 
    | Cons _ x xs => vect_eq_nat _ (app (rev' xs) (Cons _ x Nil)) 
    end. 
Solve Obligation 0 using (intros; omega).