Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: 2013 Q5


David Renshaw (Jan 17 2021 at 03:29):

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 (Jan 17 2021 at 03:30):

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

Heather Macbeth (Jan 17 2021 at 03:43):

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

David Renshaw (Jan 17 2021 at 03:45):

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

David Renshaw (Jan 17 2021 at 03:46):

I wanted to put some effort into cleanup first.

Alex J. Best (Jan 17 2021 at 03:58):

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 (Jan 17 2021 at 04:08):

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 (Jan 17 2021 at 04:22):

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

Heather Macbeth (Jan 17 2021 at 04:36):

docs#geom_sum₂_mul ?

David Renshaw (Jan 17 2021 at 04:39):

ah, nice!

David Renshaw (Jan 17 2021 at 20:10):

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

Bryan Gin-ge Chen (Jan 17 2021 at 20:17):

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 (Jan 17 2021 at 20:28):

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 (Jan 17 2021 at 20:35):

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 (Jan 17 2021 at 20:46):

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 (Jan 17 2021 at 21:15):

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 (Jan 18 2021 at 02:26):

@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 (Jan 18 2021 at 02:34):

@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 (Jan 18 2021 at 02:34):

(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...)


Last updated: Dec 20 2023 at 11:08 UTC