Coq中的異構列表

我正在考慮編寫一個Coq程序來驗證relational algebra的某些屬性。我有一些基本的數據類型工作，但連接元組給我帶來一些麻煩。Coq中的異構列表

這裏是代碼的相關章節：

Require Import List. 
Require Import String. 

(* An enum representing SQL types *) 
Inductive sqlType : Set := Nat | Bool. 

(* Defines a map from SQL types (which are just enum values) to Coq types. *) 
Fixpoint toType (t : sqlType) : Set := 
    match t with 
    | Nat => nat 
    | Bool => bool 
    end. 

(* A column consists of a name and a type. *) 
Inductive column : Set := 
    | Col : string -> sqlType -> column. 

(* A schema is a list of columns. *) 
Definition schema : Set := list column. 

(* Concatenates two schema together. *) 
Definition concatSchema (r : schema) (s : schema) : schema := app r s. 

(* Sends a schema to the corresponding Coq type. *) 
Fixpoint tuple (s : schema) : Set := 
    match s with 
    | nil => unit 
    | cons (Col str t) sch => prod (toType t) (tuple sch) 
    end. 

Fixpoint concatTuples {r : schema} {s : schema} (a : tuple r) (b : tuple s) : tuple (concatSchema r s) := 
    match r with 
    | nil => b 
    | cons _ _ => (fst a , concatTuples (snd a) b) 
    end.

在功能concatTuples，在零的情況下，CoqIDE給我的錯誤：

"The term "b" has type "tuple s" while it is expected to have type "tuple (concatSchema ?8 s)"."

我想我明白髮生了什麼有;類型檢查器不能發現s和concatSchema nil s是相等的。但我發現離奇的是，當我添加以下行：

Definition stupid {s : schema} (b : tuple s) : tuple (concatSchema nil s) := b .

和的情況下更改爲nil => stupid b，它的工作原理。（當然，它仍然在抱怨的利弊情況，但我認爲，這意味着它接受零的情況下）。

我對這個三個問題：

是否有消除stupid的方法嗎？ Coq似乎知道類型是平等的，它只是需要某種提示。
我怎麼可以做cons case呢？編寫類似stupid的函數時遇到了很多麻煩。
這甚至是異構列表的正確方法嗎？這對我來說似乎是最直接的一個，但我對科裏 - 霍華德的掌握非常寬鬆，以及Coq代碼的實際含義。

來源

2015-04-02 Henry Swanson

我會盡量避免這麼多，呃，「型變種」。 – Atsby 2015-04-02 02:54:44

你究竟是什麼意思？ – 2015-04-02 02:56:54

這是Coq新手最經常遇到的問題之一：無法顯示Coq如何使用在match聲明的分支中獲得的附加信息。

的解決方案是使用所謂的convoy pattern，再抽象依賴於你的scrutinee的參數，使您的match返回一個函數：

Fixpoint concatTuples {r : schema} {s : schema} : tuple r -> tuple s -> tuple (concatSchema r s) := 
    match r return tuple r -> tuple s -> tuple (concatSchema r s) with 
    | nil => fun a b => b 
    | cons (Col _ t) _ => fun a b => (fst a, concatTuples (snd a) b) 
    end.

在這種特殊情況下，return標註不實際上需要，因爲科克可以推斷出來。但是，當事情有點不對時，忽略它往往會導致不可理解的錯誤消息，所以將它們留在它們中是一個不錯的主意。注意，我們還必須在我們列表的第一個元素（Col _ t模式）中包含嵌套匹配，，以模仿tuple定義中的模式。再一次，CPDT詳細解釋了這裏發生了什麼，以及如何在Coq中編寫這種函數。

要回答你的最後一個問題，許多開發異構列表或多或少地以你在這裏做的相同的方式列出（例如，我有one development，這與這個非常相似）。如果我不得不改變任何東西，我會刪除tuple定義中的嵌套模式，這樣可以在使用較少的match es和註釋時編寫此類代碼。比較：

Definition typeOfCol c := 
    match c with 
    | Col _ t => t 
    end. 

(* Sends a schema to the corresponding Coq type. *) 
Fixpoint tuple (s : schema) : Set := 
    match s with 
    | nil => unit 
    | cons col sch => prod (toType (typeOfCol col)) (tuple sch) 
    end. 

Fixpoint concatTuples {r : schema} {s : schema} : tuple r -> tuple s -> tuple (concatSchema r s) := 
    match r return tuple r -> tuple s -> tuple (concatSchema r s) with 
    | nil => fun a b => b 
    | cons _ _ => fun a b => (fst a, concatTuples (snd a) b) 
    end.

你可以找到這個問題here和here的其他例子。

來源

2015-04-02 03:01:52

Coq中的異構列表

回答

相關問題