Prove that the only zero-length vector is nil

Question

I have a type defined as

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

and I'm trying to prove:

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

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

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?

Answer 1

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.

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.

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.

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 *)

Answer 2

Here is a simple proof (borrowed from this Coq Club thread):

Definition emptyIsAlwaysNil {a: bits 0} : a = bitsNil :=
  match a with bitsNil => eq_refl end.

Opaque emptyIsAlwaysNil.

Here is what Coq builds under the hood:

Print emptyIsAlwaysNil.

emptyIsAlwaysNil = 
fun a : bits 0 =>
match
  a as a0 in (bits n)
  return
    (match n as x return (bits x -> Type) with
     | 0 => fun a1 : bits 0 => a1 = bitsNil
     | S n0 => fun _ : bits (S n0) => IDProp
     end a0)
with
| bitsNil => eq_refl
| bitsCons _ _ => idProp
end
     : forall a : bits 0, a = bitsNil