How to use Fin n?

Stream: new members

[George Tsoukalas]

Hi, I am trying to write in Lean a statement like the following:

section
variable (n : ℕ)
example (f : Fin n → ℕ) (h : ∀ k, f k ≠ 0) : ∑ i : Fin n, f i ≠ 0 := sorry

#eval ∑ i : Fin 5, i

While this doesn't throw any errors, the #eval line outputs 2, not 10. I am not sure how to interpret this - is i : Fin 4 a single element drawn from Fin 4? For this reason I am not sure if I can reason about the goal to prove correctly. Also, in the proof of the example I can write

example (f : Fin n → ℕ) (h : ∀ k, f k ≠ 0) : ∑ i : Fin n, f i ≠ 0 := by
  have h' := h 3

which returns the message "failed to synthesize instance OfNat (Fin n) 3". I also tried replacing Fin with Finset.range , in which case the evaluation of the sum

#eval ∑ i in Finset.range 5, i

returns 10, the correct value, but

example (f : Finset.range n → ℕ) (h : ∀ k, f k ≠ 0) : ∑ i in Finset.range n, f i ≠ 0 := sorry

complains that "application type mismatch f i argument i has type \N : Type but is expected to have type { x // x ∈ range n } : Type. Does anyone know what the correct way to do this is? It's not just about computing the sum but also indexing a finite set of elements, in this case annotated via f.

[Sophie Morel]

The inhabitants of Fin n are not just the integers from 0 to n-1, they are couples formed by an integers i and a proof that i is less than n.
So for example, you'll get the correct sum if you write:

#eval ∑ i : Fin 5, i.1

[Sophie Morel]

In your second example, you cannot apply f to 3 because 3 is not of type Fin n, it is of type Nat.

[Sophie Morel]

variable (n : ℕ)

open BigOperators in
example (f : Fin n → ℕ) (h : ∀ k, f k ≠ 0) : ∑ i : Fin n, f i ≠ 0 := by
  rw [← Nat.pos_iff_ne_zero]
  apply Finset.sum_pos (fun k _ ↦ Nat.pos_iff_ne_zero.mpr (h k))
  -- Here to conclude we need `Fin n` to be nonempty, hence `n` to be positive.

[Eric Wieser]

Another spelling you can use is #eval ∑ i : Fin 5, (i : ℕ)

[Sophie Morel]

To finish the example:

open BigOperators in
example (f : Fin n → ℕ) (h : ∀ k, f k ≠ 0) (hn : n > 0) : ∑ i : Fin n, f i ≠ 0 := by
  rw [← Nat.pos_iff_ne_zero]
  apply Finset.sum_pos (fun k _ ↦ Nat.pos_iff_ne_zero.mpr (h k))
  existsi ⟨0, hn⟩

[Sophie Morel]

The last line proves that Finset.univ of Fin n is nonempty by providing an element. Note how I had to write the element as a couple with entries 0 and the proof that 0 < n.

[George Tsoukalas]

Sophie Morel said:

variable (n : ℕ)

open BigOperators in
example (f : Fin n → ℕ) (h : ∀ k, f k ≠ 0) : ∑ i : Fin n, f i ≠ 0 := by
  rw [← Nat.pos_iff_ne_zero]
  apply Finset.sum_pos (fun k _ ↦ Nat.pos_iff_ne_zero.mpr (h k))
  -- Here to conclude we need `Fin n` to be nonempty, hence `n` to be positive.

Makes sense. Is it generally most natural to use Fin for these kinds of formalizations?

[Sophie Morel]

I'm not sure I'm an expert, but I would say that it depends a lot on the context anyway (like where your function f comes from, and how you will use the positivity of the sum).

[Sophie Morel]

By the way, you got the unexpected #eval results because Fin n also has an addition, but it's addition mod n. That is what your #eval lines were calculating.

[Yaël Dillies]

Usually it's better to have f : ℕ → something, h : ∀ k < n, something_else (f k) and ∑ k in Finset.range n, f k

[George Tsoukalas]

Sophie Morel said:

By the way, you got the unexpected #eval results because Fin n also has an addition, but it's addition mod n. That is what your #eval lines were calculating.

Ah, that makes a lot of sense! Thank you!

[George Tsoukalas]

Yaël Dillies said:

Usually it's better to have f : ℕ → something, h : ∀ k < n, something_else (f k) and ∑ k in Finset.range n, f k

I was concerned about doing something like this because I am not sure how automation like aesop or duper might handle working in a "larger" space if they are converting the statement to something an SMT solver can digest. Do you happen to know if that a reasonable concern?

[Yaël Dillies]

aesop currently is rubbish at handling quantifiers (universal quantifiers in hypotheses and existential quantifiers in the goal), so I don't think that's much of a concern