# Zulip Chat Archive

## 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 `n`

is 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