Proving empty vector is nil

Stream: general

[Jordan Mitchell Barrett]

Suppose I have a type family vec parametrised by its length n : nat:

constant A : Type

inductive vec : nat -> Type
| nil : vec 0
| cons {n:nat} : vec n -> A -> vec (n.succ)

Now, I want to show that any vec 0 has to be nil:

theorem vec_zero_is_nil (v : vec 0) : v = vec.nil

I can't work out how to prove this, though. The obvious way seems to be to destruct v. The cons case gives an easy contradiction, but in the nil case, I get a hypothesis v == vec.nil. What does this == mean, and how can I deduce that v = vec.nil?

[Mario Carneiro]

The usual way to spell coq's destruct in lean is cases and it seems to do the right thing here:

theorem vec_zero_is_nil (v : vec 0) : v = vec.nil :=
by { cases v, refl }

[Kyle Miller]

Somewhat amusingly, this is one of those cases where Lean already knows it can only be vec.nil:

constant A : Type

inductive vec : nat -> Type
| nil : vec 0
| cons {n:nat} : vec n -> A -> vec (n.succ)

theorem vec_zero_is_nil : Π (v : vec 0), v = vec.nil
| vec.nil := rfl

This is relying on the equation compiler doing case analysis and building the proof for you. In this case, I think it deduces that 0 = n.succ has no solutions since nat.succ is injective.

[Kyle Miller]

The == is heterogeneous equality. It appears when you have terms of equal types, and it's usually something you want to avoid since it's rather weak. However, in this case both the terms involved have the same type (not merely equal) so eq_of_heq will do. (For the second case, I'm forgetting what I'm supposed to do, so I used the low-level nat.no_confusion. The exfalso is not necessary here.)

theorem vec_zero_is_nil (v : vec 0) : v = vec.nil :=
begin
  destruct v,
  { intros he h,
    apply eq_of_heq h, },
  { intros n w a hz,
    exfalso,
    exact nat.no_confusion hz, },
end