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 中，在 nil 的情况下，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，就可以了。（好吧，它仍然在 cons 情况下抱怨，但我认为这意味着它正在接受 nil 情况。）

关于这个我有三个问题：

有没有办法消除stupid？似乎 Coq 知道类型是相等的，它只需要某种提示。
cons case 到底该怎么做？我在编写类似 stupid 的函数时遇到了很多麻烦。
这甚至是处理异构列表的正确方法吗？对我来说这似乎是最直接的一个，但我对 Curry-Howard 以及 Coq 代码的实际含义了解得非常松散。

Answer 1

这是 Coq 新手最常遇到的问题之一：无法向 Coq 展示如何使用在 match 语句的分支中获得的附加信息。

解决方案是使用所谓的convoy pattern，重新抽象化依赖于你的监督者的参数，让你的matchreturn成为一个函数：

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 定义中的嵌套模式，这允许您在编写此类代码时使用更少的 matches 和注释。比较：

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 and 。

Coq 中的异构列表

Heterogeneous list in Coq

coq

convoy-pattern