Zulip Chat Archive

Stream: new members

Topic: using patterns in eq compiler


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 21 2020 at 19:59):

There's probably a better way.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:06):

Sorry, what is enumerate from supposed to do?

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:07):

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

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:07):

Yeah, or define an inductive version of vector.

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:09):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 20:09):

That's exactly fin n

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:10):

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

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:10):

not in my mathlib! fin is just a subtype

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:10):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:11):

Oh right. fin2 is the inductive version of fin.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))
-/

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 20:12):

using a small has_repr (fin n) that I wrote

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 21 2020 at 20:41):

What would be the type of vector.filter?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Oct 21 2020 at 21:08):

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

view this post on Zulip 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
/-
♞, ♞, ♘, ♘
-/

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 21:11):

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

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 21:11):

The proof term for the filtering is the magic rfl

view this post on Zulip Yakov Pechersky (Oct 21 2020 at 21:11):

and __ is just option.none


Last updated: May 08 2021 at 18:17 UTC