类型族的归纳定义

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"组成的。当然我需要定义一些将 Language r 的元素转换为 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

幸运的是，无需求助于 Coq 基本逻辑之外的特征就可以证明 l0，只需对前面引理的陈述做一个小改动即可。

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 return 上进行匹配，这是一个在 v 上抽象的函数。这是所谓的 "convoy pattern" 的另一个实例。如果我们写了

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

Coq 会将 0 分支中的 v 视为具有类型 Vector.t A n，从而使该分支类型错误。

提出这样的概括是在 Coq 中进行依赖类型编程的一大难题。其他系统，例如 Agda，可以更轻松地编写此类代码，但直到最近 shown 才可以在不依赖 Coq 想要避免包含在其代码中的额外公理的情况下完成此操作基础理论。我们只能希望在以后的版本中能简化这一点。

类型族的归纳定义

Inductive definition for family of types

coq