类型族的归纳定义

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

幸运的是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

这里发生了什么？这个问题,粗略地说,就是在勒柯克我们不能依赖类型,它们的指数具有特定的形状方面进行案例分析(如0,你的情况)直接.相反,我们必须证明一个更普遍的陈述,其中有问题的指数被变量所取代.这正是l0_gen引理所做的.注意我们如何在n返回一个抽象的函数时进行匹配v.这是所谓的"护卫模式"的另一个例子.我们写的

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

Coq会v在0分支中看到有类型Vector.t A n,使得该分支生病.

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