How do I convince the Lean 4 type checker that addition is commutative?

Question

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the example in TPiL as:

inductive Vector (α : Type u) : Nat → Type u
  | nil  : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n+1)

I tried implementing an append function to concatenate two vectors as

def append : Vector α m → Vector α n → Vector α (m + n)
  | nil, v => v
  | cons h t, v => cons h (append t v)

but in the nil case I get the error

type mismatch
  v
has type
  Vector α n : Type ?u.1240
but is expected to have type
  Vector α (0 + n) : Type ?u.1240

The type checker apparently can't tell that Vector α n and Vector α (0 + n) are the same type. It works if I instead change the type of append to Vector α m → Vector α n → Vector α (n + m), so that the expected type is Vector α (n + 0). So apparently it can't tell that addition is commutative.

If I do change the type to Vector α (n + m), then later when I use it to implement a function to reverse a vector it fails to type check again:

def reverse : {n : Nat} -> Vector α n → Vector α n
  | 0, nil => nil
  | n' + 1, cons h t => append (reverse t) (cons h nil)

The reason is that on the recursive call it expects reverse t to be of type Vector α 1 and cons h nil to be of type Vector α n' (rather than the other way around) so that the result will have type Vector α (n' + 1) (rather than Vector α (1 + n')). So again the problem is that it doesn't realize that addition is commutative.

What do I have to do to get the type checker to understand that Vector α (m + n) is the same as Vector α (n + m)?

Answer 1

Type theories typically have a two notions of equality. There is a "definitional" equality corresponding roughly to syntactic (so "external") equality modulo conversion rules (particularly beta-reduction). There is also a "propositional" equality represented by a type and terms inside the theory (the type family = in Lean). The propositional equality is "really" equality (e.g. you can prove 0 + n = n), and the more restricted definitional equality is what the type checker uses when comparing "expected" and "actual" types (here, it can't show 0 + n is definitionally equal to 0, because the definition of + is such that 0 + n does not reduce/simplify.)

Reflecting propositional equality to definitional equality (i.e. "convincing the type checker" of more equalities) is not possible in Lean, nor most theorem provers, since it makes type checking undecidable. Instead† you have the ability to "rewrite" or "substitute" according to a propositional equality: If you have proved p : x = y and you have a : P x then you can get p ▸ a : P y. That is, you explicitly take your term and "move it" along an equality. The type checker still considers x and y to be different, and p ▸ a is also different from a (unless y is definitionally x and p is definitionally refl, in which case p ▸ a is definitionally a).

Pulling lemmas for 0 + n = n and m + 1 + n = m + n + 1 from the standard library (that these are nontrivial is why the checker isn't trusted with handling them implicitly):

def append : {m : Nat} → Vector α m → Vector α n → Vector α (m + n)
  | 0, nil, ys => Eq.symm (Nat.zero_add n) ▸ ys -- I think ▸ is supposed to handle symming for you when necessary; not sure why it fails here...
  | m + 1, cons x xs, ys => Nat.succ_add m n ▸ cons x (append xs ys) -- outer goal Vector α (m + 1 + n), inner goal Vector α (m + n + 1)

Note that I have to add m to the matching in order to be able to pass it to one of the theorems.

†In actuality you usually have an induction principle for =, which is more general than just substitution. In Lean 4 ▸ is a (builtin) macro that uses this induction principle.