IMO formalization

Stream: new members

[Nick_adfor]

Let S be the set of real numbers greater than -1. Find all functions f : S → S such that f ( x + f ( y ) + x f ( y ) ) = y + f ( x ) + y f ( x ) for all x and y in S , and f ( x ) / x is strictly increasing for -1 < x < 0 and for x > 0 .

I try to formalize the problem as follows.

import Mathlib

theorem imo_1994_p5 (S : Set ℝ) (f : ℝ → ℝ) (hS : S = Set.Ioi (-1 : ℝ)) :
    (∀ x y, x ∈ S → y ∈ S → f (x + f y + x * f y) = y + f x + y * f x) ∧
    (∀ x, x ∈ S → x ≠ 0 → StrictMonoOn (fun x => f x / x) (Set.Ioo (-1) 0) ∧ StrictMonoOn (fun x => f x / x) (Set.Ioi 0))  →
    ∃! f, ∀ x, x ∈ S → f x = -x / (1 + x) := by sorry

But an error occurs in the last line:
f x = -x / (1 + x)

Infoview tells me that:

function expected at
  f
term has type
  ?m.925

Is there something wrong with the definition of x or f?

[Ruben Van de Velde]

Double $'s for latex on zulip

[Nick_adfor]

Ruben Van de Velde said:

Double $'s for latex on zulip

I've editted it containing only unicode. The latex here is too hard to use. I do not even know how to type Latex here.

[Sabbir Rahman]

here's the fixed syntax code

import Mathlib

theorem imo_2006_p3 (S : Set ℝ) (f : ℝ → ℝ) (hS : S = Set.Ioi (-1 : ℝ)) :
    (∀ x y, x ∈ S → y ∈ S → f (x + f y + x * f y) = y + f x + y * f x) ∧
    (∀ x, x ∈ S → x ≠ 0 → StrictMonoOn (fun x => f x / x) (Set.Ioo (-1) 0) ∧ StrictMonoOn (fun x => f x / x) (Set.Ioi 0))  →
    ∃! f: ℝ → ℝ, ∀ x, x ∈ S → f x = -x / (1 + x) := by sorry

the issue is that in target, f represents the bound f from ∃! f. And since you did not specify any type there, lean assumed metavariable type ?m.1489

[Sabbir Rahman]

But even if code is syntacticaly correct, I feel like you shouldn't use f in target as that'll override f from hypothesis. which you don't want to do

[Nick_adfor]

Sabbir Rahman said:

But even if code is syntacticaly correct, I feel like you shouldn't use f in target as that'll override f from hypothesis. which you don't want to do

Thank you! What should I do to completely get rid of the target (I mean not only in code, but also in mind)? As you say, the target will produce some contradictory/override.

Since I do not begin to write the proof code, I do not want to have any bug from the target in the future : (

[Sabbir Rahman]

When you have (f : ℝ → ℝ) in hypothesis that already defines a function. So in that case I feel like target should be something like f = fun x: ℝ => -x / (1+x) as that states the function is -x/(1+x)upto equality

you could also try a different way to formulate where the statement would just be a big ∃! f that states f satisfies required properties and also f x = -x/(1+x) for all x. I do feel like first way is more natural

[Joseph Myers]

imo_2006_p3 is a rather eccentric choice of name for IMO 1994 P5! If you're interested in seeing how someone else has done it, there's a complete formal solution in Compfiles.

[Nick_adfor]

Joseph Myers said:

imo_2006_p3 is a rather eccentric choice of name for IMO 1994 P5! If you're interested in seeing how someone else has done it, there's a complete formal solution in Compfiles.

Well, thanks (imo_2006_p3 is just a nick name as my name : )
I check the Compfiles which I don't know before: https://github.com/dwrensha/compfiles/blob/main/Compfiles/Imo1994P5.lean
It is of good help! And the code writer even define his own ProblemExtraction.lean, which truly surprises me.

[Nick_adfor]

To lake build compfile needs long time!

[Kevin Buzzard]

Did you get mathlib cache first?

[Kevin Buzzard]

If I type lake exe cache get in the repo and then lake build then the build finishes in just under 1 minute on my machine.

[Nick_adfor]

[Quoting…]

Wow, I take longer because of my old computer : ( But it has finished now.
By the way, is there any other IMO(or other competition formalization) packages? I have an interest to learn to write formalization like them. Model packages are needed.