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

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.

之后intros，我已经试过constructor 1，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".

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

Answer 1

是的，你基本上是正确的：具体来说，不是类型检查的是 Coq 试图构造一个matchon a:bits 0（这就是case）：bitsCons案例有一个类型错误的结论。

这是一个无公理证明。关键的想法是手动将语句概括为任何内容n = 0（我不知道如何使用策略来做到这一点；它们都因依赖性而失败）。然后，等式证明会进行结论类型检查，无论是什么n，我们都可以驳回这种bitsCons情况，因为我们将得到n = S n'。在更困难的bitsNil情况下，我们使用eq_rect_eq_dec，这是 Axiom K 的结果，但当类型索引（nat在本例中为 ）具有可判定的相等性时，它是可证明的。请参阅Coq 标准库文档，了解无需可判定相等公理即可完成的其他一些操作。

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（请参阅CPDT 的等式章节了解更多详细信息），则可以更简单地证明该定理，因为那时您可以使用dependent inductionor dependent destruction：

Require Import Program.Equality.

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

Lemma emptyIsAlwaysNil :
  forall {a: bits 0}, a = bitsNil.
Proof.
  intros.
  dependent destruction a; reflexivity.
Qed.

Print Assumptions emptyIsAlwaysNil.
(* Axioms:
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y *)