Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: 2013 Q5


view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip David Renshaw (Jan 17 2021 at 03:45):

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

view this post on Zulip David Renshaw (Jan 17 2021 at 03:46):

I wanted to put some effort into cleanup first.

view this post on Zulip 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:

view this post on Zulip 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)))

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Jan 17 2021 at 04:36):

docs#geom_sum₂_mul ?

view this post on Zulip David Renshaw (Jan 17 2021 at 04:39):

ah, nice!

view this post on Zulip David Renshaw (Jan 17 2021 at 20:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Aug 05 2021 at 04:14 UTC