证明唯一的零长度向量为nil [英] Prove that the only zero-length vector is nil

问题描述

我的类型定义为

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 之后，我尝试了构造函数1 ，情况a ，直觉，无济于事。 a案例似乎是最接近的案例，但是会出现错误：

After intros, I've tried constructor 1, case a, intuition, to no avail. case a seems like the closest, but it gets an error:

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".

听起来好像无法确定任意长度的位向量是否等于1长度为零，因为它们在类型级别上有所不同。

It sounds like it can't determine whether a bit-vector of an arbitrary length is equal to one of zero-length, because they're different at the type level. Is that correct?

推荐答案

是的，您基本上是正确的：具体地说，类型检查不是Coq的尝试构建 a上的匹配：位0 （这是情况确实）： bitsCons 案的结论不正确。

Yes, you're basically correct: specifically, what isn't type checking is Coq's attempt to construct a match on a:bits 0 (which is what case does): the bitsCons case has an ill-typed conclusion.

这里是无公理证明。关键思想是将语句手动推广为任何 n = 0 （我不知道该如何使用战术；它们都依赖于依赖项）。然后，相等证明将检查结论类型，而不考虑 n 是什么，并且我们可以驳回 bitsCons 的情况，因为'将有 n = S n'。在更困难的 bitsNil 情况下，我们使用 eq_rect_eq_dec ，这是公理K的结果，但在类型索引（在本例中为 nat ）具有可判定的相等性。请参阅 Coq标准库文档，了解其他一些您可以不用做的事情具有确定性的公理。

Here's an axiom-free proof. The key idea is to manually generalize the statement to any n = 0 (I couldn't figure out how to do this with tactics; they all trip up on the dependency). The equality proof then makes the conclusion type check regardless of what n is, and we can dismiss the bitsCons case because we'll have n = S n'. In the more difficult bitsNil case, we make use of eq_rect_eq_dec, which is a consequence of Axiom K but is provable when the type index (nat, in this case) has decidable equality. See the Coq standard library documentation for some other things you can do without axioms with decidable equality.

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.

您不需要x中的 rew H EqNotations 中的c>表示法（它只是包装了 eq_rect ，等式递归原理），但是我发现它使事情变得很重要

You don't need the rew H in x notation from EqNotations (it just wraps eq_rect, the equality recursion principle), but I find it makes things much more readable.

但是，如果您愿意使用公理，尤其是 JMeq_eq （有关更多详细信息，请参见 CPDT的平等章节），这样您就可以使用依赖性诱导或依赖性破坏：

However, you can prove this theorem more simply if you're willing to use an axiom, specifically JMeq_eq (see CPDT's equality chapter for more details), since then you can use dependent induction or 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 *)

这篇关于证明唯一的零长度向量为nil的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！