Lean won't let me write proposition due to type error

Stream: new members

[aron]

I've got this definition of a Vec and an append function:

inductive Vec (α : Type u) : (len : Nat) → Type u
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

def Vec.append {α : Type} {n m : Nat} (xs : Vec α n) (ys : Vec α m) : Vec α (n + m) :=
  match xs with
  | Vec.nil => by simp; exact ys
  | Vec.cons x xs' =>
    by
    have newTails := Vec.append xs' ys
    have newVec := Vec.cons x newTails
    rewrite [Nat.add_right_comm]
    exact newVec

Now I'm trying to write a theorem that appending an empty vec with another vec is the same as that other vec:

theorem Vec.append_nil_left {α : Type} {n : Nat} (xs : Vec α n) : Vec.append Vec.nil xs = xs := by sorry

But Lean won't even let me write down the proposition because

type mismatch
  xs
has type
  Vec α n : Type
but is expected to have type
  Vec α (0 + n) : Type

Because this error is in the proposition itself I can't even use Nat.zero_add to explain that these are equivalent. How can I fix this type error?

[Damiano Testa]

This is a possible way out, but I do not know how workable it is:

def Vec.append {α : Type} {n m nm : Nat} (hnm : nm = n + m) (xs : Vec α n) (ys : Vec α m) : Vec α nm :=
  match xs with
  | Vec.nil => by simp [hnm]; exact ys
  | Vec.cons x xs' =>
    by
    have newTails := Vec.append rfl xs' ys
    have newVec := Vec.cons x newTails
    rewrite [hnm, Nat.add_right_comm]
    exact newVec

theorem Vec.append_nil_left {α : Type} {n : Nat} (xs : Vec α n) : Vec.append n.zero_add.symm Vec.nil xs = xs := by
  sorry

[aron]

but I want Vec.append to just take two vecs as input, I don't want to have to pass a separate hnm and evidence that hnm = n + m

[aron]

I don't even understand what the problem here is, since lean has no problem with clearly nonsensical propositions like 1 = 0

[Damiano Testa]

The problem is that the target type contains 0 + n which is propositionally equal to n but not definitionally equal to it. So, the formula that you are trying to prove does not type check: Eq requires the two sides to be definitionally equal and they are not.

[Johannes Tantow]

Lean does not know that 0+n is equal to n. 0+nis not definitionally equalt to n since addition for natural number recurses in the second argument. Note that

theorem Vec.append_nil_right {α : Type} {n : Nat} (xs : Vec α n) : Vec.append xs Vec.nil = xs := by sorry

typechecks as now the second argument in the addition is zero. You can fix your statement by casting it:

theorem Vec.append_nil_left {α : Type} {n : Nat} (xs : Vec α n) : cast (by simp) (Vec.append Vec.nil xs) = xs := by sorry

[Kyle Miller]

Please don't use the top-level cast for this — it's too general in practice.

Here's an example of how to write a custom cast function to be able to write nil_append: #new members > Vector nil_append @ 💬 (This is all inside the Vector namespace)

[Kyle Miller]

aron said:

I don't even understand what the problem here is, since lean has no problem with clearly nonsensical propositions like 1 = 0

When there's a type mismatch error, it's saying that the types are not definitionally equal. You need definitionally equal types for the = operator to make sense.

There's nothing wrong with 1 = 0 because both 1 and 0 are Nat. As far as Lean is concerned, in append_nil_left you are writing something like true = (). The types are Bool and Unit here, which are not definitionally equal.

[Edward van de Meent]

Kyle Miller said:

The types are Bool and Unit here, which are not definitionally equal.

as a matter of fact, they are provably not equal, since they have different cardinalities.