2

我正在考虑编写一个 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 中，在 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 代码的实际含义有一个非常松散的理解。
4

1 回答 1

3

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

解决方案是使用所谓的convoy 模式，重新抽象取决于您的审查员的参数并使您的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 中编写这种函数。

为了回答您的最后一个问题，异构列表的许多开发或多或少与您在此处所做的方式相同（例如，我有一个与此非常相似的开发）。如果我必须更改任何内容，我会删除定义中的嵌套模式，这样您就可以在使用更少的es 和注释tuple的情况下编写此类代码。match比较：

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.

您可以在此处和此处找到有关此问题的其他示例。

于 2015-04-02T03:01:52.403 回答