vector exercise from Leroy's lectures

Stream: general

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Damn you Carneiro, I needed four lines :-)

[Kevin Buzzard]

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

[Koundinya Vajjha]

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

[Kevin Buzzard]

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.

[Kenny Lau]

I think you can omit the second line

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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