using patterns in eq compiler

Stream: new members

[Yakov Pechersky]

What would be the right syntax to get something like the following to work?

import data.vector2

variables {α β : Type*} {n m : ℕ}

lemma list.length_cons_tail {x : α} {l : list α} (h : (x :: l).length = n + 1) : l.length = n :=
by { simpa only [add_left_inj, list.length] using h }

def vector.my_map_l : Π {n : ℕ}, vector α n → (α → β) → vector β n
| 0       _           _ := vector.nil
| (n + 1) ⟨x :: l, h⟩ f := f x ::ᵥ (vector.my_map_l ⟨l, list.length_cons_tail h⟩ f)

local attribute [pattern] vector.cons

-- this does not work
def vector.my_map_v : Π {n : ℕ}, vector α n → (α → β) → vector β n
| 0       _         _ := vector.nil
| (n + 1) (x ::ᵥ v) f := f x ::ᵥ (vector.my_map_v v f)

[Adam Topaz]

I had to give lean a hint that nis smaller than n+1, but here it is:

import data.vector2

variables {α β : Type*} {n m : ℕ}

lemma list.length_cons_tail {x : α} {l : list α} (h : (x :: l).length = n + 1) : l.length = n :=
by { simpa only [add_left_inj, list.length] using h }

def vector.my_map_l : Π {n : ℕ}, vector α n → (α → β) → vector β n
| 0       _           _ := vector.nil
| (n + 1) ⟨x :: l, h⟩ f := f x ::ᵥ (vector.my_map_l ⟨l, list.length_cons_tail h⟩ f)

local attribute [pattern] vector.cons

def vector.my_map_v : Π {n}, vector α n → (α → β) → vector β n
| 0 _ _ := vector.nil
| (n+1) vs f := have n < n + 1, from lt_add_one n,
    (f vs.head) ::ᵥ vector.my_map_v vs.tail f

[Adam Topaz]

There's probably a better way.

[Yakov Pechersky]

Thanks!

So I can just directly do:

def vector.my_map_v : Π {n : ℕ}, vector α n → (α → β) → vector β n
| 0       _ _ := vector.nil
| (n + 1) v f := f v.head ::ᵥ vector.my_map_v v.tail f

[Adam Topaz]

Oh yeah that works. I don't know why lean was telling at me about well_founded_recursion.

[Yakov Pechersky]

Really, I'm defining the following:

def vector.enumerate_from {α : Type*} : Π {n} m : ℕ, vector α n → vector (fin (m + n) × α) n
| 0       _ _           := vector.nil
| (n + 1) m v := (⟨m, (lt_add_iff_pos_right m).mpr nat.succ_pos'⟩, v.head) ::ᵥ
                           (vector.map (prod.map fin.succ id) (vector.enumerate_from m v.tail))

[Yakov Pechersky]

And it's not clear for me whether things of this nature should be expressed as variations of vector.map_accumr or map_accuml (which doesn't even exist yet), or do bespoke definitions each time

[Yakov Pechersky]

Unfortunately, while the m + n order makes this definition easier, it makes it that the following is a little nastier than desired:

def vector.enumerate {α : Type*} {n : ℕ} (v : vector α n) : vector (fin n × α) n :=
vector.map (prod.map (fin.cast (zero_add n)) id) $ vector.enumerate_from 0 v

[Yakov Pechersky]

it's either rely on the defeq of n + 0 in the enumerate defn, or in the enumerate_from

[Kevin Buzzard]

inb4 Mario -- the problem with types like vector α n is that they're dependent types, which should be avoided at all costs in dependent type theory.

[Adam Topaz]

Sorry, what is enumerate from supposed to do?

[Kevin Buzzard]

i.e. "use lists if you possibly can"

[Adam Topaz]

Yeah, or define an inductive version of vector.

[Adam Topaz]

E.g.

universe u
inductive my_vector (α : Type u) : ℕ → Type u
| nil : my_vector 0
| cons : α → my_vector n → my_vector (n+1)

[Adam Topaz]

I feel like something like that already exists somewhere in mathlib, no?

[Yakov Pechersky]

That's exactly fin n

[Adam Topaz]

I thought fin n := {x : \N // x < n}.

[Kevin Buzzard]

not in my mathlib! fin is just a subtype

[Kevin Buzzard]

It's very close to fin2 n though...

[Yakov Pechersky]

/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple -/
def cons (x : α 0) (p : Π(i : fin n), α (i.succ)) : Πi, α i :=
λ j, fin.cases x p j

[Kevin Buzzard]

/-- An alternate definition of `fin n` defined as an inductive type
  instead of a subtype of `nat`. This is useful for its induction
  principle and different definitional equalities. -/
inductive fin2 : ℕ → Type
| fz {n} : fin2 (succ n)
| fs {n} : fin2 n → fin2 (succ n)

[Adam Topaz]

Oh right. fin2 is the inductive version of fin.

[Yakov Pechersky]

Using lists is fine, until you have to provide a proof to list.nth_le, otherwise list.nth returns an option a

[Yakov Pechersky]

So either you carry around the proof all the time, or invent it at the time of list.nth_le

[Yakov Pechersky]

#eval vector.nth $ vector.enumerate_from 5 $
  (vector.of_fn (![some 1, some 2, some 6, none, some 10]))
/-
(5, (some 1)), (6, (some 2)), (7, (some 6)), (8, none), (9, (some 10))
-/

[Yakov Pechersky]

using a small has_repr (fin n) that I wrote

[Adam Topaz]

I think it would be easier to define this for lists and prove separately that the list version of enumerate_from preserves the length, which would let you extend it to vectors.

[Adam Topaz]

Of course, this requires knowing how vectors are defined, which might upset some people.

[Yakov Pechersky]

Totally. I just spent ~300 lines defining vector.filter, and it was that long because I was trying to work with the underlying list as little as possible.

[Adam Topaz]

Alternatively, it's possible to define a general induction principle for vectors, with a type similar to list.rec and use that as your recursor.

[Adam Topaz]

What would be the type of vector.filter?

[Yakov Pechersky]

def vector.filter_count : ℕ := (v.to_list.filter p).length

def vector.filter (h : v.filter_count p = m) : vector α m :=
⟨v.to_list.filter p, h⟩

[Yakov Pechersky]

With a final culmination in

lemma vector.filter_valid (hm : v.filter_count p = m) : ∀ i, p ((v.filter p hm).nth i) :=
begin
  cases n,
  { have hm' : m = 0,
      { simpa only [vector.filter_count_nil] using hm.symm },
    unify_equations hm',
    exact fin_zero_elim },
  { cases m,
    { exact fin_zero_elim },
    { rw vector.prop_distribute',
      have hx : p (v.filter p hm).head,
        { refine vector.filter_count_imp_head _ _ (le_refl (m + 1)),
          simp only [vector.filter_count_filter] },
      simp only [hx, true_and],
      apply vector.filter_count_imp_tail,
      simp only [vector.filter_count_filter] } }
end

[Yakov Pechersky]

Of course, it'd be much easier to prove the validity by accessing the underlying list, but where is the fun in that?

[Adam Topaz]

Oh ok, I was just wondering how you were handling the length.

[Yakov Pechersky]

Yeah, passing around a proof of it and using it. So in practical use, it looks like:

#eval vector.nth $ vector.reduce_some (vector.of_fn $ matrix.ravel
      (![![(♞ : option (chess.colored_pieces)), __, ♞],
         ![__, __, __],
         ![♘, __, ♘]])) rfl
/-
♞, ♞, ♘, ♘
-/

[Yakov Pechersky]

Where you can fill in the expected "function" of unknown functions, in that example.

[Yakov Pechersky]

The proof term for the filtering is the magic rfl

[Yakov Pechersky]

and __ is just option.none