Vacuously true?

Stream: lean4

[Dax Fohl]

I just started with Lean yesterday. I want to prove sum(1..n) = n(n+1)/2, by e.g. sum [1,2,3,4] + sum [4,3,2,1] = sum [1+4, 2+3, 3+2, 4+1] = sum [5,5,5,5] = 4*5.

So I've got a first_n_nat that returns vector e.g. [4, 3, 2, 1].

def first_n_nat : (n: Nat) → Vector Nat n
| (Nat.zero) => Vector.nil
| (Nat.succ n) => Vector.cons (Nat.succ n) (first_n_nat n)

I have a proof that the sum of the reverse is equal to the sum of the original. Now I just want to prove that each kth element of that vector has value n - k.

theorem first_n_nat_k_eq_n_sub_k (n: Nat) (k: Fin n):
  (first_n_nat n).get k = (n - k) := by
    induction n with
    | zero => sorry
    | succ nn ih => sorry

But the base case is vacuously true? There's no k for Fin zero. But I don't see a way to do that. Or maybe I shouldn't be using induction here? Seems silly I can't figure out how to prove this step, since it's almost by definition.

[Ruben Van de Velde]

docs#Fin.elim0 might help you

[Dax Fohl]

Yeah I saw that function and thought it looked relevant, but can't figure out how it's supposed to be used. I've tried lots of variants around zero => rw [Fin.elim0] but nothing has worked.

[Ruben Van de Velde]

Maybe apply Fin.elim0 x

[Calvin Lee]

Specifically, the exact term you need is Fin.elim0 k

[Calvin Lee]

(so exact k.elim0 would work as well)

[Jireh Loreaux]

I think the more idiomatic way to prove your result while preserving your proof technique is to use docs#Finset.sum_range_reflect with f := (fun n ↦ (n + 1 : ℤ)).