Zulip Chat Archive

Stream: maths

Topic: Help {generalize, rename} these lemmas for mathlib


Mark Gerads (Sep 22 2022 at 19:11):

I needed these simple lemmas, and was unable to find them in the library.
Before these lemmas can be added to mathlib, they need to be generalized.
I would like some help with that. Whoever helps can take full credit by making the GitHub commit if they wish.
Also, the lemmas need to be renamed to mathlib style.

import analysis.special_functions.trigonometric.basic

lemma cpowIntExponentSplitBase (z1 z2:) (n:) : (z1 * z2) ^ n = z1 ^ n * z2 ^ n:=
begin
  induction n with n ih,
  simp only [pow_zero, mul_one],
  rw [pow_succ,pow_succ,pow_succ],
  have h: z1 * z1 ^ n * (z2 * z2 ^ n) = z1 * z2 * (z1 ^ n * z2 ^ n),
    ring,
  rw h,
  congr' 1,
end

lemma cpowIntExponentSplitExponent (z1:) (n k:) : z1 ^ (n + k) = z1 ^ n * z1 ^ k:=
begin
  induction k with k ih,
  simp only [add_zero, pow_zero, mul_one],
  have h: k.succ =  k + 1,
  simp only [eq_self_iff_true],
  rw [pow_succ, h],
  have h2: n + (k + 1) = (n+k)+1,
  simp only [add_comm, add_assoc],
  rw h2,
  have h3: n + k + 1=(n + k).succ,
  simp only [eq_self_iff_true],
  rw [h3, pow_succ],
  have h4: z1 ^ n * (z1 * z1 ^ k) = z1 * (z1 ^ n * z1 ^ k),
  ring,
  rw h4,
  congr' 1,
end

lemma cpowIntTimesIntExponent (z1:) (n k:) : z1 ^ (n * k) = (z1 ^ n) ^ k:=
begin
  induction k with k ih,
  simp only [mul_zero, pow_zero],
  rw [pow_succ],
  have h: n * k.succ = n*(k+1),
    simp only [eq_self_iff_true],
  rw h,
  have h2: n * (k + 1) = n+n*k,
    ring,
  rw h2,
  have h3:z1 ^ (n + n * k) = z1 ^ n * z1 ^ (n * k),
    exact cpowIntExponentSplitExponent z1 n (n * k),
    rw h3,
  congr' 1,
end

Alex J. Best (Sep 22 2022 at 19:15):

docs#mul_pow, docs#pow_add, docs#pow_mul I believe. I think will save time if assume that lemmas of this level are in mathlib already (things like this generally are) and look for them with library_search or the naming convention or #Is there code for X? first

Mark Gerads (Sep 22 2022 at 19:26):

Nice; this will make my file smaller. I tried library_search, but didn't ask at #Is there code for X? .
Maybe library_search!needs to be improved?

Alex J. Best (Sep 22 2022 at 19:30):

Hmm library search works fine for me for the first one at least. Though I would say the naming convention is even faster

Mark Gerads (Sep 22 2022 at 19:34):

Interesting. I double-checked that library_search! did not result in anything before making this post. Checking again now, the cause is (deterministic) timeout.

Jireh Loreaux (Sep 22 2022 at 19:38):

This is the #naming that Alex is referring to. With this consistency in naming, many simple lemmas can be found just by guessing and using the autocomplete feature in VS Code (or in the API documentation). However, if there is something that you think should exist, but can't find, definitely ask in #Is there code for X? first. Simple things especially don't bother to try and reprove.

Jireh Loreaux (Sep 22 2022 at 19:39):

For example, if you want a lemma to say that a - b - c = a - (b + c), you can easily guess that this will be called docs#sub_sub.

Alex J. Best (Sep 22 2022 at 19:40):

Ah yes, deterministic timeout isnt a fair per se, just that there are too many lemmas to check with your imports, for the purposes of library search its helpful to set it a bit higher than the default, https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout.

Newell Jensen (Sep 22 2022 at 19:41):

Curious what others have set their memory limits at who have done so...

Newell Jensen (Sep 22 2022 at 19:42):

Or rather, not the exact limits, but if they have found this to actually be beneficial and have noticed a marked difference.

Mark Gerads (Sep 22 2022 at 19:46):

I changed the Lean settings to have a memory limit of 39000 (most of my RAM), and now library_search! works for all 3 lemmas. I will need to remember this next time I reinstall Linux.

Newell Jensen (Sep 22 2022 at 19:48):

Mark Gerads said:

I changed the Lean settings to have a memory limit of 39000 (most of my RAM), and now library_search! works for all 3 lemmas. I will need to remember this next time I reinstall Linux.

Good to know! Thanks.

Jireh Loreaux (Sep 22 2022 at 19:48):

If you are regularly hitting timeouts during development (with the standard heartbeat limit of 100000), in my experience it either means (a) that you are working on some very complicated stuff, or (b) you need to find ways to make your code more efficient and/or idiomatic (e.g., squeezing simps). I just wrote a rather long and complicated proof while using the standard timeout and didn't hit it.

Alex J. Best (Sep 22 2022 at 19:50):

I dont think the memory limit should affect library search, only the timeout.

Alex J. Best (Sep 22 2022 at 19:52):

And while that's definitely true Jireh I do find it useful to write a slow proof that works and then speed it up when its done. Something like double the default timeout is normally enough for me

Mark Gerads (Sep 22 2022 at 19:54):

Alex J. Best said:

I dont think the memory limit should affect library search, only the timeout.

I did not change the timeout, only the memory, so counter-example.

Jireh Loreaux (Sep 22 2022 at 20:40):

Alex, I see what you mean, and that can be useful in certain circumstances. However, if I'm constantly hitting 100000 heartbeats in a proof that isn't super complex, then I'm spending too much time waiting for Lean to compile every step and I should speed up the proof early anyway to save myself time developing. I guess if you have a very fast machine this is less of an issue, but I'm frequently working on my laptop with only 4 cores.

Jireh Loreaux (Sep 22 2022 at 20:41):

sometimes having the timeout higher can be useful when squeezing simps though.


Last updated: Dec 20 2023 at 11:08 UTC