Vector nil_append

Stream: new members

[sgcs]

I'm trying to prove some things about the vector data type but occasionally run into problems dealing with the vector size in type definitions. For example, I have the following code:

universe u v w

inductive Vector (α : Type u) : Nat → Type u where
  | nil : Vector α 0
  | cons {n : Nat} : α → Vector α n → Vector α (Nat.succ n)

infixr:67 " :: " => Vector.cons

namespace Vector

def append {α : Type u} {m n : Nat} : Vector α m → Vector α n → Vector α (m + n)
  | nil, ys => by simp only [Nat.zero_add]; exact ys
  | x :: xs, ys => by
      simp only [Nat.succ_add]
      exact cons x (append xs ys)

@[simp]
theorem nil_append {n : Nat} {α : Type} (as : Vector α n) : @Eq (Vector α n) (append (@nil α) as) as := by sorry

How do I define nil_append in a type correct way? If I could use Nat.zero_add in the function definition, the types would match but not sure how to proceed.

[sgcs]

I've tried something like this:

@[simp]
theorem nil_append {n : Nat} {α : Type} (as : Vector α n) : @Eq (Vector α n) ((@Eq.mp (Vector α (0 + n)) (Vector α n) (by simp) (append (@nil α) as))) as := by sorry

It ypechecks, but I'm not really sure how to prove it with the cast present. And it doesn't seem like it would be useful the way it's defined (at the very least, nil ++ xs doesn't seem to simplify in other places)

[Kyle Miller]

Here are two places in mathlib that implement a pattern to solve this sort of issue: docs4#SimpleGraph.Walk.copy
docs4#Quiver.Hom.cast

[Kyle Miller]

The idea would be that you define a Vector.cast function that takes an equality that swaps out the size of the array with something else. This is just Eq.rec under the hood but it helps keep the rewrites circumscribed to just the size (otherwise you're liable to get equalities of types, which aren't great)

[Kyle Miller]

For example, in the Vector namespace:

def cast (v : Vector α m) (h : m = n) : Vector α n := h ▸ v

@[simp] theorem cast_rfl (v : Vector α m) : v.cast rfl = v := rfl

@[simp] theorem cast_cast (v : Vector α m) (h : m = m') (h' : m' = m'') :
    (v.cast h).cast h' = v.cast (h.trans h') := by subst_vars; rfl

[Kyle Miller]

Then this typechecks:

@[simp]
theorem nil_append {n : Nat} {α : Type} (as : Vector α n) :
  append nil as = as.cast (Nat.zero_add n).symm := by sorry

[Kyle Miller]

With a new version of append that makes use of cast, nil_append is a one-liner:

def append {α : Type u} {m n : Nat} : Vector α m → Vector α n → Vector α (m + n)
  | nil, ys => ys.cast (by simp [Nat.succ_add])
  | x :: xs, ys => (cons x (append xs ys)).cast (by simp only [Nat.succ_add])

@[simp]
theorem nil_append {n : Nat} {α : Type} (as : Vector α n) :
    append nil as = as.cast (Nat.zero_add n).symm := by
  cases as <;> simp [append]

[Floris van Doorn]

Since + on Nat is defined by recursion on the second argument, I strongly recommend that you define Vector.append also by recursion on the second argument. This allows you to define it without any casts. Of course, to state nil_append you still have to use casts or heterogenous equality.

[Kyle Miller]

Vector.cons also needs to add elements to the end of the list to be able to implement Vector.append efficiently if you're inducting on the second argument. (Or we need to go back to the drawing board and refine Nat.add to induct on the first argument too :smile:)

[Floris van Doorn]

You're right, this would need an snoc operation...

[Kyle Miller]

Re HEq: this is another way to state nil_append, and HEq can sometimes be more convenient than cast. The downsides are (1) you can't rewrite with a HEq lemma and (2) the HEq doesn't "know" that the sizes are equal, unlike cast which records that equality.

[Eric Rodriguez]

i think you are able to extract the equality of types and therefore sizes from the HEq

[Kyle Miller]

I think using only type equalities, from Vector Nat m you can only tell whether m is zero or nonzero, since m is zero if and only if the type is a singleton and m is nonzero if and only if the type is countable.

[Eric Rodriguez]

Ah, yes, the constructor isn't necessarily injective on types unless alpha is a fintype.

[Eric Rodriguez]

I wonder if stating that those families are disjoint is possible in type theories