证明唯一的零长度向量是零

Question

我有一个类型定义为

Inductive bits : nat -> Set :=
| bitsNil : bits 0
| bitsCons : forall {l}, bool -> bits l -> bits (S l).

而我正试图证明：

Lemma emptyIsAlwaysNil : forall {a: bits 0}, a = bitsNil.

在qazxsw poi之后，我尝试了qazxsw poi，qazxsw poi，qazxsw poi，但无济于事。 intros似乎是最接近的，但它得到一个错误：

constructor 1

听起来它无法确定任意长度的位向量是否等于零长度的位向量，因为它们在类型级别上是不同的。那是对的吗？

Answer 1

是的，你基本上是正确的：具体来说，什么不是类型检查是Coq试图在case a上构建一个intuition（这是case a所做的）：

Abstracting over the terms "0" and "a" leads to a term
fun (n : nat) (a0 : bits n) => a0 = bitsNil
which is ill-typed.
Reason is: Illegal application: 
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "bits n" : "Set"
 "a0" : "bits n"
 "bitsNil" : "bits 0"
The 3rd term has type "bits 0" which should be coercible to 
"bits n".

案例有一个错误的结论。

这是一个无公理的证明。关键的想法是手动将语句概括为任何match（我无法弄清楚如何用策略做到这一点;他们都会依赖于依赖）。然后，无论a:bits 0是什么，等式证明都会得出结论类型检查，我们可以解雇case案例，因为我们将有bitsCons。在更加困难的n = 0案例中，我们使用n，这是Axiom K的结果，但是当类型索引（在这种情况下为bitsCons）具有可判定的相等性时，它是可证明的。查看n = S n'，了解其他一些事情，如果没有具有可判定平等的公理，你可以做些什么。

bitsNil

你不需要来自eq_rect_eq_dec的nat表示法（它只包括Coq standard library documentation，等式递归原理），但我发现它使事情更具可读性。

但是，如果你愿意使用公理，特别是

Require PeanoNat.
Require Import Eqdep_dec.
Import EqNotations.

Inductive bits : nat -> Set :=
| bitsNil : bits 0
| bitsCons : forall {l}, bool -> bits l -> bits (S l).

Lemma emptyIsAlwaysNil_general :
  forall n (H: n = 0) {a: bits n},
    rew [bits] H in a = bitsNil.
Proof.
  intros.
  induction a; simpl.
  (* bitsNil *)
  rewrite <- eq_rect_eq_dec; auto.
  apply PeanoNat.Nat.eq_dec.
  (* bitsCons - derive a contradiction *)
  exfalso; discriminate H.
Qed.

Lemma emptyIsAlwaysNil : forall {a: bits 0},
    a = bitsNil.
Proof.
  intros.
  change a with (rew [bits] eq_refl in a).
  apply emptyIsAlwaysNil_general.
Qed.

（更多细节参见rew H in x），你可以更简单地证明这个定理，从那以后你可以使用EqNotations或eq_rect：

JMeq_eq

Answer 2

这是一个简单的证据（借用CPDT's equality chapter）：

dependent induction

以下是Coq在引擎盖下构建的内容：

dependent destruction