Неопределенный список в Coq

Question

Я рассматриваю возможность написания программы Coq для проверки определенных свойств relational algebra. У меня есть некоторые из основных типов данных, но конкатенация кортежей дает мне некоторые проблемы.

Вот соответствующий раздел кода:

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, это работает. (Ну, это все еще жалуется на случае минусов, но я думаю, что означает, что он принимая ноль случая.)

У меня есть три вопроса по этому поводу:

1. Есть ли способ устранить stupid? Кажется, что Coq знает, что типы равны, ему просто нужен какой-то намек.
2. Как я могу сделать дело «против»? У меня много проблем с записью функции stupid.
3. Это даже правильный подход к гетерогенным спискам? Мне кажется, что это самый простой для меня, но у меня очень свободное понимание Карри-Говарда, и то, что на самом деле означает код Coq.

Answer 1

Это один из самых повторяющихся проблем для новичков в 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 аннотаций не на самом деле необходимо, поскольку Coq может это сделать. Тем не менее, опускание может часто приводить к непонятным сообщениям об ошибках, когда что-то идет не так, так что это хорошая идея оставить их. Обратите внимание, что мы должны были также включать вложенный матч в первый элемент нашего списка (шаблон 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.