2013 Q5

Stream: IMO-grand-challenge

[David Renshaw]

It took me two weeks, but I now finally have a proof for Q5 from IMO 2013:

theorem imo2013Q5
  (f: ℚ → ℝ)
  (f_i:  ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
  (f_ii: ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
  (f_iii: ∃ a, 1 < a ∧ f a = a)
  : ∀ x, 0 < x → f x = x

https://github.com/dwrensha/mathematical-puzzles-in-lean/blob/master/src/imo2013_q5.lean

[David Renshaw]

(The code could definitely use some cleaning up, and I probably am doing some silly noobish things.)

[Heather Macbeth]

Will you contribute it to the repository? https://github.com/leanprover-community/mathlib/tree/master/archive/imo

[David Renshaw]

Yes, I'd like to eventually submit a pull request.

[David Renshaw]

I wanted to put some effort into cleanup first.

[Alex J. Best]

Wow, cool!
Looks like you've (re)proved quite a few library lemmas though like your nth_power_gt_one would follow from docs#one_lt_pow or nat_abs_pos would be a one-liner from docs#nat_abs_pos_of_ne_zero I believe, hope you didn't spend too long on those! It's true that the library does have many gaps, but for lemmas like those I would usually assume they are already in the library somewhere, finding them can be tough though of course :smile:

[David Renshaw]

does mathlib have anything that I could have used instead of this lemma?

lemma factor_xn_m_yn
      (x : ℝ)
      (y:ℝ)
      (n: ℕ)
      :  x^n - y^n = (x - y) * (∑ (i:ℕ) in finset.range n, (x ^(i) * y ^(n - 1 -i)))

[Alex J. Best]

There is docs#polynomial.pow_sub_pow_factor but its not quite the same I think?

[Heather Macbeth]

docs#geom_sum₂_mul ?

[David Renshaw]

ah, nice!

[David Renshaw]

I've submitted https://github.com/leanprover-community/mathlib/pull/5786.

[Bryan Gin-ge Chen]

Thanks! I've sent you an invite to the mathlib repo. Please open a PR from a branch on the mathlib repo per the instructions here.

[David Renshaw]

I'm having trouble running the linter locally:

$ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
Traceback (most recent call last):
  File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 212, in <module>
    lint(Path(fn))
  File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 206, in lint
    errs = reserved_notation_check(lines, fn)
  File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 87, in reserved_notation_check
    if fn.relative_to(ROOT_DIR) == Path('src/tactic/reserved_notation.lean'):
  File "/usr/lib64/python3.9/pathlib.py", line 928, in relative_to
    raise ValueError("{!r} is not in the subpath of {!r}"
ValueError: 'src/logic/embedding.lean' is not in the subpath of '/home/dwrensha/src/mathlib' OR one path is relative and the other is absolute.

[Bryan Gin-ge Chen]

Hmm, it's failing for me too for an unrelated reason:

$ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
++ find . -name '*.lean' -type f -executable
find: -executable: unknown primary or operator
+ executable_files=

I guess the version of find in my version of macOS doesn't support -executable.

@Julian Berman #5721 was supposed to make it easier to run the linter, right? Want to take a look?

[Alex J. Best]

This is quite weird, on my setup (MINGW64 on windows) using the fixes suggested at
https://apple.stackexchange.com/questions/116367/find-all-executable-files-within-a-folder-in-terminal don't work, maybe using an approach like
https://github.com/npryce/adr-tools/commit/3dcf8388900a10c6bf6ea35e45a44758e6cd1a24
is most portable?

[Julian Berman]

Bryan Gin-ge Chen said:

Hmm, it's failing for me too for an unrelated reason:

$ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
++ find . -name '*.lean' -type f -executable
find: -executable: unknown primary or operator
+ executable_files=

I guess the version of find in my version of macOS doesn't support -executable.

Julian Berman #5721 was supposed to make it easier to run the linter, right? Want to take a look?

Oy, yes will have a look in a few hours

[Julian Berman]

@David Renshaw an immediate fix is this diff:

⊙  g diff                                                                                                                                                                                                                                                                                                                                                      julian@Home ●
diff --git a/scripts/lint-style.sh b/scripts/lint-style.sh
index d20887efd..5d00a6a4a 100755
--- a/scripts/lint-style.sh
+++ b/scripts/lint-style.sh
@@ -35,7 +35,7 @@ set -exo pipefail

 touch scripts/style-exceptions.txt

-find src archive -name '*.lean' | xargs ./scripts/lint-style.py
+find $PWD/src $PWD/archive -name '*.lean' | xargs ./scripts/lint-style.py

 # 2. Global checks on the mathlib repository

i.e. to add $PWD/ in front of archive and src in lint-style.sh.

I'll send a PR to mathlib to fix, but given I've broken it once already and CI passed, I think it deserves a few unit tests to make sure I'm not breaking any other combination of absolute/relative, so will take me a day or so to get that sent over.

[Julian Berman]

@Bryan Gin-ge Chen if you're adventurous, you can use GNU find on macOS. (I do, it works fine, and only once in a blue moon do I need to tell something to use regular BSD find). brew install findutils and then placing it first on your PATH.

[Julian Berman]

(Though yeah that sounds worth fixing too... will have a look tomorrow when I poke around more. Possibly the whole thing can just be a Python script...)