Fin and positivity error

Stream: new members

[Alex Gu]

I am formalizing a problem as such:

import Mathlib

theorem no_positive_terms (n : ℕ) (a : Fin n → ℕ)
  (h_n : n ≥ 3)
  (h_endpoints : a 0 = 0)
  (h_ineq : ∀ k, 1 ≤ k ∧ k < n-1 → a (k-1) + a (k+1) ≥ 2*a k) :
  ∀ i, i < n → a i ≤ 0 := by
  sorry

This doesn't work, presumably because it's unhappy that I'm using a 0 when n is a natural number that could be 0 (even though I have h_n). Is the preferred workaround for this to use n : ℕ+? Or a : Fin (n+1) → ℕ?

[Kevin Buzzard]

My instinct is (a) never ever ever use natural subtraction unless you absolutely have to (so no k-1) and (b) there's no point having a natural t and a hypothesis t >= r, you may as well use a natural t' := t - r with no hypothesis. With those design decisions in mind I get

import Mathlib

-- let n' = n - 3
theorem no_positive_terms (n' : ℕ) (a : Fin (n' + 3) → ℕ)
  (h_endpoints : a 0 = 0)
  -- let k' = k - 1
  (h_ineq : ∀ k', k' ≤ n' → a k' + a (k'+2) ≥ 2*a (k' + 1)) :
  ∀ i, i < n' + 3 → a i ≤ 0 := by
  sorry

which does work (although the result doesn't look true to me, why can't a(t) be t?)

[Alex Gu]

In cases where you have to do natural number subtraction, would you operate everything with integers? For example, if I wanted to prove something like "for positive integers n, prove that n-n^2<0", would you express it like(n : ℤ) (h : n > 0)? though this violates your principle (b)

[Kevin Buzzard]

This doesn't violate (b) because there's no natural in sight. Yes this looks fine although mathematically it's also incorrect