Prove that the only zero-length vector is nil

Link:

https://stackoverflow.com/q/47945424

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:

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:

The command has indeed failed with message:
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 (Tej Chajed)

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


forall (n : nat) (H : n = 0) (a : bits n),
rew [bits] H in a = bitsNil


forall (n : nat) (H : n = 0) (a : bits n),
rew [bits] H in a = bitsNil

  
n: nat
H: n = 0
a: bits n
rew [bits] H in a = bitsNil
 
H: 0 = 0
rew [bits] H in bitsNil = bitsNil
l: nat
H: S l = 0
b: bool
a: bits l
IHa: forall H : l = 0, rew [bits] H in a = bitsNil
rew [bits] H in bitsCons b a = bitsNil

  
H: 0 = 0
rew [bits] H in bitsNil = bitsNil

    
H: 0 = 0
bitsNil = bitsNil
H: 0 = 0
forall x y : nat, {x = y} + {x <> y}
 
H: 0 = 0
forall x y : nat, {x = y} + {x <> y}

    apply PeanoNat.Nat.eq_dec.
  
l: nat
H: S l = 0
b: bool
a: bits l
IHa: forall H : l = 0, rew [bits] H in a = bitsNil
rew [bits] H in bitsCons b a = bitsNil

    exfalso; discriminate H.
Qed.


forall a : bits 0, a = bitsNil


forall a : bits 0, a = bitsNil

  
a: bits 0
a = bitsNil

  
a: bits 0
rew [bits] eq_refl in a = bitsNil

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


forall a : bits 0, a = bitsNil


forall a : bits 0, a = bitsNil

  
a: bits 0
a = bitsNil
 dependent destruction a; reflexivity.
Qed.


Axioms:
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y

Answer (Anton Trunov)

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:

emptyIsAlwaysNil = 
fun a : bits 0 =>
match
  a as a0 in (bits n)
  return
    (match n as x return (bits x -> Prop) 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

Arguments emptyIsAlwaysNil {a}

A: Reminds me of Monin's small inversions: hal.archives-ouvertes.fr/inria-00489412