类型族的归纳定义

Question

我已经为此苦苦挣扎了一段时间。我有一个归纳类型：

Definition char := nat.
Definition string := list char.


Inductive Exp : Set :=
  | Lit : char -> Exp
  | And : Exp -> Exp -> Exp
  | Or  : Exp -> Exp -> Exp
  | Many: Exp -> Exp

我从中归纳定义了一系列类型：

Inductive Language : Exp -> Set :=                                                                                                                                          
  | LangLit     : forall c:char, Language (Lit c)
  | LangAnd     : forall r1 r2: Exp, Language(r1) -> Language(r2) -> Language(And r1 r2)
  | LangOrLeft  : forall r1 r2: Exp, Language(r1) -> Language(Or r1 r2)
  | LangOrRight : forall r1 r2: Exp, Language(r2) -> Language(Or r1 r2)
  | LangEmpty   : forall r: Exp, Language (Many r)
  | LangMany    : forall r: Exp, Language (Many r) -> Language r -> Language (Many r).

这里的理由是，给定一个正则表达式r:Exp，我试图将与r 关联的语言表示为Language r 类型，并且我使用单个归纳定义来这样做。

我想证明：

Lemma L1 : forall (c:char)(x:Language (Lit c)),
  x = LangLit c.

(也就是说Language (Lit c)类型只有一个元素，即正则表达式'c'的语言是由单个字符串"c"组成的。当然我需要定义@的一些语义转换元素987654330@转string)

现在这个问题的细节并不重要，只是用来激发我的问题：让我们使用nat而不是Exp，让我们定义一个类型List n，它代表长度为n的列表：

Parameter A:Set.
Inductive List : nat -> Set :=
  | ListNil   : List 0
  | ListCons  : forall (n:nat), A -> List n -> List (S n).

这里我再次使用一个归纳定义来定义一系列类型List n。

我想证明：

Lemma L2: forall (x: List 0),
  x = ListNil.

（换句话说，List 0 类型只有一个元素）。

我已经没有关于这个的想法了。

通常当尝试用归纳类型（或谓词）证明（否定）结果时，我会使用elim 策略（确保所有相关假设都在我的目标之内（generalize）并且只有变量出现在类型构造函数）。但是elim在这种情况下就不行了。

Answer 1

如果您愿意接受的不仅仅是 Coq 的基本逻辑，您可以使用 dependent destruction 策略，该策略可在 Program 库中找到（我冒昧地将您的上一个示例改写为标准库向量）：

Require Coq.Vectors.Vector.

Require Import Program.

Lemma l0 A (v : Vector.t A 0) : v = @Vector.nil A.
Proof.
now dependent destruction v.
Qed.

如果您检查该术语，您会发现该策略依赖于 JMeq_eq 公理来获得通过的证明：

Print Assumptions l0.

Axioms:
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y

幸运的是，通过对前面引理的陈述做一点小改动，就可以证明l0，而不必求助于 Coq 基本逻辑之外的功能。

Lemma l0_gen A n (v : Vector.t A n) :
  match n return Vector.t A n -> Prop with
  | 0 => fun v => v = @Vector.nil A
  | _ => fun _ => True
  end v.
Proof.
now destruct v.
Qed.

Lemma l0' A (v : Vector.t A 0) : v = @Vector.nil A.
Proof.
exact (l0_gen A 0 v).
Qed.

我们可以看到这个新证明不需要任何额外的公理：

Print Assumptions l0'.
Closed under the global context

这里发生了什么？粗略地说，问题在于，在 Coq 中，我们不能直接对索引具有特定形状（例如 0，在您的情况下）的依赖类型的术语执行案例分析。相反，我们必须证明一个更一般的陈述，其中有问题的索引被变量替换。这正是l0_gen 引理正在做的事情。请注意我们必须如何使n 上的匹配返回一个抽象v 的函数。这是所谓的"convoy pattern" 的另一个实例。如果我们写了

match n with
| 0 => v = @Vector.nil A
| _ => True
end.

Coq 会在 0 分支中看到 v 的类型为 Vector.t A n，从而使该分支为错误类型。

提出这样的概括是在 Coq 中进行依赖类型编程的一大难题。其他系统，例如 Agda，可以用更少的努力编写这种代码，但直到最近 shown 才可以在不依赖 Coq 想要避免包含在其基本理论中的额外公理的情况下做到这一点.我们只能希望这将在未来的版本中得到简化。