Zulip Chat Archive

Stream: general

Topic: vector exercise from Leroy's lectures


view this post on Zulip Kevin Buzzard (Jun 28 2019 at 09:13):

inductive xfin :   Type
| zero :  n, xfin (nat.succ n)
| succ :  n, xfin n  xfin (nat.succ n)

inductive vec (A : Type) :   Type
| nil : vec 0
| cons :  n, A  vec n  vec (nat.succ n)

def mth (A : Type) (n : ) (v : vec A n) (m : xfin n) : A := sorry

Slightly trickier than I expected, but I got there in the end. Returns the m'th element of the vector.

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 09:21):

Unit tests:

#eval mth  2 (vec.cons 1 4 (vec.cons 0 6 (vec.nil ))) (xfin.zero 1) -- 4
#eval mth  2 (vec.cons 1 4 (vec.cons 0 6 (vec.nil ))) (xfin.succ 1 (xfin.zero 0)) -- 6

view this post on Zulip Mario Carneiro (Jun 28 2019 at 09:47):

def mth (A : Type) :  (n : ), vec A n  xfin n  A
| _ (vec.cons n a l) (xfin.zero _) := a
| _ (vec.cons _ a l) (xfin.succ n i) := mth n l i

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 11:00):

Damn you Carneiro, I needed four lines :-)

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 11:01):

Oh wait -- your answer is better than mine: I needed to use ._ (I think). Unfortunately my answer is at home right now.

view this post on Zulip Koundinya Vajjha (Jun 28 2019 at 11:08):

I'm surprised while writing this you didn't cause lean to segfault. I faced the same problem a few days ago.
https://github.com/leanprover-community/lean/issues/52

view this post on Zulip Kevin Buzzard (Jun 29 2019 at 21:35):

def mth (A : Type) : Π (n : ) (v : vec A n) (m : xfin n), A
| 0 v m := by cases m
| (d+1) (vec.cons ._ a w) (xfin.zero ._) := a
| (d+1) (vec.cons ._ a w) (xfin.succ ._ e') := mth d w e'

was my answer.

view this post on Zulip Kenny Lau (Jun 30 2019 at 08:40):

I think you can omit the second line

view this post on Zulip Kevin Buzzard (Jun 30 2019 at 18:16):

Right -- the equation compiler is smart enough to do the cases, it seems.

view this post on Zulip Kevin Buzzard (Jun 30 2019 at 18:19):

def mth (A : Type) : Π (n : ) (v : vec A n) (m : xfin n), A
| _ (vec.cons _ a _) (xfin.zero _) := a
| _ (vec.cons _ _ w) (xfin.succ _ e') := mth _ w e'

I think that's the sup of what you can omit

view this post on Zulip Mario Carneiro (Jun 30 2019 at 18:20):

The ._ inaccessible patterns seem to be optional now, ever since leo made some change to the way the equation compiler handles these things

view this post on Zulip Mario Carneiro (Jun 30 2019 at 18:21):

which is useful since it's hard to know how to use them properly


Last updated: May 15 2021 at 23:13 UTC