Avoiding type-level unfolding in functional definitions

Stream: general

[Kat Zhuchko]

I am using the following inductive definition of a vector:

inductive Vect (α : Type) : (n : Nat) → Type where
  | nil : Vect α 0
  | cons : α → Vect α n → Vect α n.succ

I want to define the filter function for vectors in a way that does not require explicit unfolding of type-level definitions.

abbrev count : (α → Bool) → Vect α n → Nat
  | p, .nil => 0
  | p, .cons x xs => (if p x then .succ else id) (count p xs)

def filter : (p : α → Bool) → (xs : Vect α n) → Vect α (count p xs)
  | p, .nil       => .nil
  | p, .cons x xs =>
    match cond : p x with
    | true  => by
      simp only [count, cond]
      exact Vect.cons x (filter p xs)
    | false => by
      simp only [count, cond]
      exact Vect.cons x (filter p xs)

Is there a nice way to do this without having to use simp?

[Kyle Miller]

I would do something like this:

inductive Vect (α : Type) : (n : Nat) → Type where
  | nil : Vect α 0
  | cons : α → Vect α n → Vect α n.succ

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

def count : (α → Bool) → Vect α n → Nat
  | p, .nil => 0
  | p, .cons x xs => (if p x then .succ else id) (count p xs)

def filter : (p : α → Bool) → (xs : Vect α n) → Vect α (count p xs)
  | p, .nil       => .nil
  | p, .cons x xs =>
    if h : p x then
      (Vect.cons x (filter p xs)).cast (by simp [count, h])
    else
      (filter p xs).cast (by simp [count, h])

I don't think it's possible to avoid unfolding count, since you need to rewrite it depending on whether or not p x is true. The only way to avoid this would be if you had some concrete p that could be evaluated by reduction. But, given that p is an unknown predicate, that can't be done.

Notice that I added a Vector.cast function. This is important, because with your version of filter, you get these rewrites of types of values, which makes working with filter much more complicated. With Vector.cast, the rewrites are safely relegated to proofs.