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

Stream: new members

[Dax Fohl]

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]

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

[Eric Wieser]

Using the match here is an error I think

[Eric Wieser]

There should be a better induction principle somewhere

[Dax Fohl]

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]

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]

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

[Eric Wieser]

docs#Fin.cases looks like it would suffice too

[Dax Fohl]

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]

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

[Dax Fohl]

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

:tada: :pray:
I don't really know what I did here but it worked! I have to imagine this could be a two-liner though if I knew what I was doing....