## Stream: new members

### Topic: using patterns in eq compiler

#### Yakov Pechersky (Oct 21 2020 at 19:30):

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 (Oct 21 2020 at 19:59):

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 (Oct 21 2020 at 19:59):

There's probably a better way.

#### Yakov Pechersky (Oct 21 2020 at 20:01):

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 (Oct 21 2020 at 20:02):

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

#### Yakov Pechersky (Oct 21 2020 at 20:03):

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 (Oct 21 2020 at 20:04):

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 (Oct 21 2020 at 20:05):

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 (Oct 21 2020 at 20:05): it's either rely on the defeq of n + 0 in the enumerate defn, or in the enumerate_from #### Kevin Buzzard (Oct 21 2020 at 20:06): 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 (Oct 21 2020 at 20:06): Sorry, what is enumerate from supposed to do? #### Kevin Buzzard (Oct 21 2020 at 20:07): i.e. "use lists if you possibly can" #### Adam Topaz (Oct 21 2020 at 20:07): Yeah, or define an inductive version of vector. #### Adam Topaz (Oct 21 2020 at 20:08): 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 (Oct 21 2020 at 20:09): I feel like something like that already exists somewhere in mathlib, no? #### Yakov Pechersky (Oct 21 2020 at 20:09): That's exactly fin n #### Adam Topaz (Oct 21 2020 at 20:10): I thought fin n := {x : \N // x < n}. #### Kevin Buzzard (Oct 21 2020 at 20:10): not in my mathlib! fin is just a subtype #### Kevin Buzzard (Oct 21 2020 at 20:10): It's very close to fin2 n though... #### Yakov Pechersky (Oct 21 2020 at 20:10): /-- 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 (Oct 21 2020 at 20:10): /-- 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 (Oct 21 2020 at 20:11): Oh right. fin2 is the inductive version of fin. #### Yakov Pechersky (Oct 21 2020 at 20:11): Using lists is fine, until you have to provide a proof to list.nth_le, otherwise list.nth returns an option a #### Yakov Pechersky (Oct 21 2020 at 20:11): So either you carry around the proof all the time, or invent it at the time of list.nth_le #### Yakov Pechersky (Oct 21 2020 at 20:12): #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 (Oct 21 2020 at 20:12): using a small has_repr (fin n) that I wrote #### Adam Topaz (Oct 21 2020 at 20:16): 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 (Oct 21 2020 at 20:17): Of course, this requires knowing how vectors are defined, which might upset some people. #### Yakov Pechersky (Oct 21 2020 at 20:19): 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 (Oct 21 2020 at 20:20): 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 (Oct 21 2020 at 20:41): What would be the type of vector.filter? #### Yakov Pechersky (Oct 21 2020 at 21:07): 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 (Oct 21 2020 at 21:08): 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 (Oct 21 2020 at 21:08): 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 (Oct 21 2020 at 21:08): Oh ok, I was just wondering how you were handling the length. #### Yakov Pechersky (Oct 21 2020 at 21:10): 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 (Oct 21 2020 at 21:11):

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

#### Yakov Pechersky (Oct 21 2020 at 21:11):

The proof term for the filtering is the magic rfl

#### Yakov Pechersky (Oct 21 2020 at 21:11):

and __ is just option.none

Last updated: May 08 2021 at 18:17 UTC