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

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 试图构建一个 match 不是类型检查的。在 a:bits 0 (这就是 case 的作用):bitsCons案件的结论错误。

这是一个无公理的证明。关键思想是手动将语句泛化到任何 n = 0 (我不知道如何用策略来做到这一点；他们都因依赖而绊倒了)。无论是什么n，等式证明都会进行结论类型检查。是，我们可以忽略 bitsCons案例，因为我们将有 n = S n' .中更难bitsNil案例，我们利用eq_rect_eq_dec ，这是 Axiom K 的结果，但是当类型索引( 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，您可以更简单地证明这个定理。 (更多细节见 CPDT's equality chapter)，从那时起你可以使用 dependent induction或 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 *)