formalizing the statement of an elementary math problem

Stream: new members

[Rado Kirov]

I was toying with formalizing some basic high school math problems from https://books.openbookpublishers.com/10.11647/obp.0181.pdf

Got stuck pretty quickly on formalizing the statement of this problem:

Screenshot 2025-10-09 at 11.47.35 PM.png

my attempt, which doesn't compile

import Mathlib

theorem p2 {n: ℕ} (x: Fin n → ℝ) (hn: 2 ≤ n) (hn: (i : Fin n) → (x i = 1 + 1 / (x (i + 1 % n)))) :
    ∀ i, x i > 1 ∧
    x 0 - x 1 = - (x 1 - x 2) / x 1 * x 2 ∧
    ∀ i, x i = x 0 := by sorry

Is there a way bake in the 2 ≤ n proof, so I can write x 0 and x 1 without errors.

[Ruben Van de Velde]

theorem p2 {n: ℕ} [NeZero n] (x: Fin n → ℝ) (hn: 2 ≤ n) (hn: (i : Fin n) → (x i = 1 + 1 / (x (Fin.ofNat n (i + 1))))) :
    ∀ i, x i > 1 ∧
    x 0 - x 1 = - (x 1 - x 2) / x 1 * x 2 ∧
    ∀ i, x i = x 0 := by sorry

seems to work

[Aaron Liu]

i + 1 means i + 1 % n

[Aaron Liu]

since it's Fin

[Ruben Van de Velde]

Oh yeah, you can just write x (i + 1). I was just trying to fix the code upthread

[Aaron Liu]

also your associativity is wrong a / b * c means (a / b) * c

[Rado Kirov]

i + 1 means i + 1 % n

oh, i didn't know that. Why just adding [NeZero n] makes all of these errors go away?
Screenshot 2025-10-10 at 7.46.50 AM.png

[Kenny Lau]

because there is no 1 in Fin 0 (indeed there is nothing in Fin 0)

[Rado Kirov]

I see, this is a great example of why [NeZero n] is useful, instead of explicit h: n > 0 which I assume will have to manually be passed everywhere.

[Vilim Lendvaj]

You don't have to manually pass it everywhere, you can do have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩ and then you can automatically pass it to other functions that already take [NeZero n], like Fin coercion.

[Thomas Preu]

Vilim Lendvaj said:

You don't have to manually pass it everywhere, you can do have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩ and then you can automatically pass it to other functions that already take [NeZero n], like Fin coercion.

How and where (before?) would you put this in the statement of the theorem?

[Kenny Lau]

with the other assumptions

[Thomas Preu]

OK, so as in the post of Ruben Van de Velde above. This is not supposed to be something global, is it?
But that only applies to [NeZero n], but not to have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩, correct?

[Kenny Lau]

yes

[Thomas Preu]

OK, so where would you use have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩ then?

[Kenny Lau]

when lean complains that it doesn't know NeZero n

[Thomas Preu]

The statement above starts with theorem p2 {n: ℕ} [NeZero n] (x: Fin n → ℝ) (hn: 2 ≤ n)
Will [NeZero n] be inferred from Hypothesis hn? Does the order matter or should hncome before [NeZero n]?

[Kenny Lau]

Thomas Preu said:

Will [NeZero n] be inferred from Hypothesis hn

you can't prove an assumption in the assumptions

[Kenny Lau]

the order does not matter, because they are independent

[Thomas Preu]

Does this mean that have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩ has to be supplied in the proof, where there is only sorry now?

[Ruben Van de Velde]

I'm not sure what your code looks like now, so that's hard to answer :)

[Ruben Van de Velde]

As a rule of thumb, you can't derive typeclass arguments ([Blah]) from normal arguments ((h : Foo))

[Thomas Preu]

I did not work with type classes so far and was completely lost on how to use them. So I curiously inquired where this have-clause would be placed. Still don't have a clue, possibly to the extent that I can't explain my loss of understanding sufficiently.

[Kevin Buzzard]

The best way to ask a question is to post some code instead of writing sentences

[Matt Diamond]

The statement above starts with theorem p2 {n: ℕ} [NeZero n] (x: Fin n → ℝ) (hn: 2 ≤ n)
Will [NeZero n] be inferred from Hypothesis hn? Does the order matter or should hncome before [NeZero n]?

I think there might be some confusion here... there's no need to infer it from hn because you already stated it as an assumption. It's not like [NeZero n] means "I can prove n is not zero". It means "n is not zero".