## Stream: new members

### Topic: kth element of [n..1] is (n-k)

#### Dax Fohl (Jul 22 2023 at 19:16):

Seems like this should be simple but I'm stuck

def first_n_nat : (n: Nat) → Vector Nat n
| 0 => Vector.nil
| n + 1 => (n + 1) ::ᵥ first_n_nat n

theorem kth_of_first_n_nat_equals_n_minus_k (n: Nat) (k: Fin n):
(first_n_nat n).get k = (n - k) := by
induction n with
| zero => exact k.elim0
| succ i ih =>
rw [first_n_nat]
match k with
| 0 => rfl
| Fin.mk (Nat.succ x) y =>
simp


It's vacuously true if n==0, and rfl works if k==0. But the remaining case leaves

i: ℕ
ih: ∀ (k : Fin i), Vector.get (first_n_nat i) k = i - ↑k
k: Fin (Nat.succ i)
x: ℕ
y: x + 1 < Nat.succ i
⊢ Vector.get ((i + 1) ::ᵥ first_n_nat i) { val := x + 1, isLt := y } = i - x


I assume I need to somehow pull the head out of the vector and subs val with x (Vector.get (first_n_nat i) { val := x, isLt := y } = i - x), but am hitting a wall with these types.

#### Eric Wieser (Jul 22 2023 at 22:40):

There should be a lemma like docs#Vector.get_cons_succ ?

#### Eric Wieser (Jul 22 2023 at 22:41):

Using the match here is an error I think

#### Eric Wieser (Jul 22 2023 at 22:41):

There should be a better induction principle somewhere

#### Dax Fohl (Jul 23 2023 at 02:18):

I'm stuck. That's very close but I can't get the { val := x + 1, isLt := y } into the Fin.succ i that Vector.get_cons_succ expects. What do you mean by a better induction principle?

#### Dax Fohl (Jul 23 2023 at 08:54):

Also by "there should be" do you mean, you think there is already one there, or there isn't but someone should make one?

#### Eric Wieser (Jul 23 2023 at 08:57):

I mean "I think there already is one"; it's docs#Fin.inductionOn

#### Eric Wieser (Jul 23 2023 at 08:58):

docs#Fin.cases looks like it would suffice too

#### Dax Fohl (Jul 23 2023 at 09:12):

Thanks again! Weird, I thought I'd looked all through that page and couldn't find an induction thing. Maybe I was looking at the wrong version.

#### Eric Wieser (Jul 23 2023 at 09:24):

I recommend using the search box for this kind of thing; typing Fin induction is enough to findit

#### Dax Fohl (Jul 24 2023 at 01:53):

theorem kth_of_first_n_nat_equals_n_minus_k (n: Nat) (k: Fin n):
(first_n_nat n).get k = (n - k) := by
induction n with
| zero => exact k.elim0
| succ i ih =>
rw [first_n_nat]
induction k using Fin.inductionOn with
| h0 => rfl
| hs =>
rw [Vector.get_cons_succ]
rw [ih]
simp