removing elements in vectors

Stream: lean4

[Frederic Peschanski]

Hello... I'm playing with vectors and I managed to implement various interesting bits.
However, I am completely stuck with the following apparently simple problem (it is a simple problem for classical lists).
First, I uses the definition of vectors found in the TPL4 book (chapter 7):

inductive Vector (A : Type u) : Nat → Type u where
  | vnil  : Vector A 0
  | vcons : A → {n : Nat} → Vector A n → Vector A (n+1)

I then define a function returning the number of occurrences of an element in a vector:

def nb_occ {A : Type} [DecidableEq A]: A → (v : Vector A n) → Nat
  | _, vnil => 0
  | a, vcons b v' => if a = b then (nb_occ a v') + 1
                                    else nb_occ a v'

And then there is the removal operation :

def vremove {A : Type} [DecidableEq A]: {n : Nat} → (a : A) → (v : Vector A n) → Vector A (n - nb_occ a v)
    -- ... my version is too ugly (and long) to show

I managed to implement this function, and test it so that it seems to be ok, although with rather
ugly proofs embarked to satisfy the return type.
... And all my tentatives to demonstrate the following theorem failed ...

theorem remove_occ {A : Type} [DecidableEq A] {n : Nat} (a : A) (v : Vector A n):
  nb_occ a (vremove a v) = 0

Of course, I have chosen this as a rather challenging exercise (ahem ... for students) ... but I challenged myself a little bit too much in the meantime. While still working on a solution, I think it is a good (if not time-consuming) exercise to play with type-level computations so I have decided to share ... the burden :sweat_smile:

[Henrik Böving]

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

def Vector.occ [DecidableEq α] (x : α) : (v : Vector α n) → Nat
  | .nil => 0
  | .cons b v' => if x = b then occ x v' + 1 else occ x v'

def Vector.remove [DecidableEq α] (r : α) (xs : Vector α n) : Vector α (n - occ r xs) :=
  match h1:xs with
  | .nil => .nil
  | @Vector.cons _ m y ys =>
    if h2 : y = r then
      let res := remove r ys
      have h3 : (m - occ r ys) = (m + 1 - occ r (cons y ys)) := sorry
      h3 ▸ res
    else
      let res := .cons y (remove r ys)
      have h3 : (m - occ r ys + 1) = (m + 1 - occ r (cons y ys)) := sorry
      h3 ▸ res

This would be my shot at a definition, theorems are left as an exercise to the reader :P (though I haven't validated they are actually provable yet myself but they sound reasonable to me)

[Frederic Peschanski]

My solution is uglier ... but without the sorry's :blush:

[Mario Carneiro]

Here's a sorry free proof using the new Std library:

import Std.Data.Nat.Lemmas

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

def Vector.occ [DecidableEq α] (x : α) : (v : Vector α n) → Nat
  | .nil => 0
  | .cons b v' => if x = b then occ x v' + 1 else occ x v'

theorem Vector.occ_le [DecidableEq α] (x : α) (v : Vector α n) : occ x v ≤ n := by
  induction v with
  | nil => apply Nat.le_refl
  | cons b v' ih =>
    simp [occ]; split
    · exact Nat.succ_le_succ ih
    · exact Nat.le_succ_of_le ih

def Vector.remove [DecidableEq α] (r : α) (xs : Vector α n) : Vector α (n - occ r xs) :=
  match xs with
  | .nil => .nil
  | @Vector.cons _ m y ys =>
    if h2 : r = y then by
      simp [occ, eq_true h2, Nat.add_sub_add_right]
      exact remove r ys
    else by
      simp [occ, h2]
      rw [Nat.sub_add_comm (Vector.occ_le ..)]
      exact .cons y (remove r ys)

[Mario Carneiro]

Of course you can write this a lot simpler if you construct the length at the same time as the vector:

def Vector.remove [DecidableEq α] (r : α) (xs : Vector α n) : Σ i, Vector α i :=
  match xs with
  | .nil => ⟨_, .nil⟩
  | Vector.cons y ys => if r = y then remove r ys else ⟨_, .cons y (remove r ys).2⟩

The type Σ i, Vector α i is basically just List α, and this function is List.filter

[Frederic Peschanski]

Thx @Mario Carneiro ! The sigma types went very smoothly as far as stating & proving theorems is concerned. However, at some point one would like to convert a ⟨n, xs⟩ of type Σ i, Vector α i to a Vector α n ... because I have other functions expecting vectors and not sigma types. But I never went that far and I can now progress so thank you again!

[Mario Carneiro]

@Frederic Peschanski you can use .2 for that

[Frederic Peschanski]

Maybe it was not clear enough, after removing all occurrences of an element in a vector, I would like to propagate in the type the fact that the size is now n - nb_occ r xs (well, going back to my initial problem).

[Mario Carneiro]

You can prove that as a theorem; that particular expression isn't likely to have good definitional properties anyway so it doesn't make much difference whether it is spelled n - nb_occ r xs or (remove r xs).1

[Frederic Peschanski]

Yeah, maybe I have the wrong perspective but maybe naively I would like to type-check and compile an expression such as:

(vappend (vremove a v1) (vremove b v2))

withvappend :: Vector A n1 -> Vector A n2 -> Vector A (n1 + n2)
Isn't this a legitimate situation ? (while playing with dependent types at least).

[Mario Carneiro]

that's fine, although you would have to write it as (vappend (vremove a v1).2 (vremove b v2).2) as I described it

[Mario Carneiro]

you could easily make vremove a v1 := (vremoveAux a v1).2 if that bothers you though

[Mario Carneiro]

but note that in that scenario (vappend (vremove a v1).2 (vremove b v2).2) would be a term of type Vector A ((vremove a v1).1 + (vremove b v2).1)

[Frederic Peschanski]

I'm not familiar with sigma types but that's convincing indeed, thank you again.

[Frederic Peschanski]

Well, I was rethinking a little bit about this.
Why for the append operation the common signature is :

vappend : Vector A n1 -> Vector A n2 -> Vector A (n1 + n2)

rather than using a dependent pairs then ?

To me, dependent pairs are useful when things can only be known at runtime, like when you want to read a vector contents from disk (this is the motivating example for dependent pairs in the Idris book). But in the removal operation the sizes and required computation are known at compile-time. Of course addition is simpler to handle than the number of occurrences of an element in a vector but it is still something you can precisely deal with.
(sorry for the insistence...)

[Kyle Miller]

When Mario said "The type Σ i, Vector α i is basically just List α", it's a strong statement -- you could even define List α to be that sigma type. So, if you define vappend using dependent pairs you have append : List A -> List A -> List A.

Many times it seems to be easier using a list type and then proving the lists have the expected lengths than to deal with the dependent type issues with vectors (for example, the non-associativity of vappend is somewhat annoying, though surmountable).

[Frederic Peschanski]

Of course, I agree for the particular case of vectors, it's not a practical example ... However the same issue would likely occur in other, more interesting situations... I mean, at some point you want to perform calculation in (dependent) types

[Frederic Peschanski]

(this is probably the old debate between internal vs. external validation ?)

[Frederic Peschanski]

(I see that my messages are inconsistent ... it is not always necessary to know things at compilation time even if it is possible, but sometimes that's what you want)

[Kyle Miller]

I wonder if what's going on with Vector is that the length of a list often isn't that important, so it's not usually worth using Vector. The Vector.remove function seems ill-matched due to how much it depends on values you might only know at runtime.

Another sort of list-like dependent type that I think is more interesting/useful is one for paths in a directed graph (a.k.a. morphisms in a category generated by some objects and arrows):

inductive Path {α : Type u} (edges : α → α → Type v) : α → α → Type (max u v)
| nil (v : α) : Path v v
| cons {u v w : α} (e : edges u v) (p : Path v w) : Path u w

Then the append function would be something of the type Path.append : Path edges u v -> Path edges v w -> Path edges u w. That is, you can only compose paths with compatible endpoints.

I saw a version of this with Haskell GADTs in the Hoopl library, to help you at compile time create well-formed basic blocks. Another situation you could use this for is having α be a type of program states and having edges u v consist of basic program steps that carry state u to state v, so then Path.append corresponds to composing two programs with compatible states.