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 案例。）

我对此有三个问题：

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

Answer 1

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

解决方案是使用所谓的convoy pattern，重新抽象依赖于你的被检查者的参数并让你的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 定义中的嵌套模式，这样您就可以在编写此类代码的同时使用更少的 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 和here 找到此问题的其他示例。