pi/2 + 2pi k

Stream: Is there code for X?

[Bolton Bailey]

Bolton Bailey said:

I spent the next forty minutes trying to prove that sin x = 1 if and only if x is of the form pi/2 + 2pi k for integer k as a lemma to another question, but after seeing that I wasn't close to this and there were other things I needed, I gave up on this one too.

Now that I can ask about this without cheating, is this in mathlib somewhere? What would've been the quick way to prove this in under an hour?

[Bolton Bailey]

docs3#real.sin_eq_sin_iff I guess

[Heather Macbeth]

The following is not a particularly clever solution, but it shows how to get there by following your nose:

example : Real.sin x = 1 ↔ ∃ k : ℤ, x = 2 * Real.pi * k + Real.pi / 2 :=
  calc Real.sin x = 1 ↔ Real.sin x = Real.sin (Real.pi / 2) := by rw [Real.sin_pi_div_two]
    _ ↔ _ := by
        rw [Real.sin_eq_sin_iff]
        constructor
        · rintro ⟨k, hk₁ | hk₂⟩
          · use - k
            push_cast
            linarith
          · use k
            push_cast
            linarith
        · rintro ⟨k, hk⟩
          use -k
          left
          push_cast
          linarith

[Heather Macbeth]

A cleverer approach is to relate to cosine:

example : Real.sin x = 1 ↔ ∃ k : ℤ, x = 2 * Real.pi * k + Real.pi / 2 := by
  rw [← Real.cos_sub_pi_div_two, Real.cos_eq_one_iff]
  congr! 1; ext k -- `congrm` not ported yet
  constructor <;> intro <;> linarith

[Joseph Myers]

I think results such as sin_eq_one_iff, cos_eq_zero_iff, sin_eq_neg_one_iff, cos_eq_neg_one_iff would clearly be appropriate for mathlib. Indeed, there are probably an enormous number of fairly basic and more or less standard facts about trigonometric functions, such as may be found on DLMF or Wikipedia, that would be appropriate for mathlib, are accessible to undergraduates (see other discussion about the presence or lack of such projects), but aren't in mathlib yet. (When you get onto hyperbolic functions, which should have many corresponding lemmas, there's even less in mathlib; we don't even have the definitions of arcosh or artanh, only arsinh, for example.)

[Heather Macbeth]

Heather Macbeth said:

A cleverer approach is to relate to cosine:

example : Real.sin x = 1 ↔ ∃ k : ℤ, x = 2 * Real.pi * k + Real.pi / 2 := by
  rw [← Real.cos_sub_pi_div_two, Real.cos_eq_one_iff]
  congr! 1; ext k -- `congrm` not ported yet
  constructor <;> intro <;> linarith

@Scott Morrison I wanted to see whether rw? could generate the beginning of this proof. It didn't find the first one -- it seems like you don't search for possible backward rewrites? Given the first one, it did find the second (ranked third on the list of proposals).

[Scott Morrison]

#mwe :-)

[Heather Macbeth]

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Tactic.Rewrites

[Scott Morrison]

Ah, so the problem here is just that rw? currently reports at most 20 results, and while it does do backwards rewrites, it penalizes them in the order scheme I used.

[Scott Morrison]

I'm recompiling weighting forward and backward rewrites equally, to see if we get something better.

[Scott Morrison]

If at some point #3973 gets some interest I will write rewrite_search in Lean 4, now that it is possible to make it fast(er). :-)

[Heather Macbeth]

Is there a prioritization scheme which is capable of observing that lemmas about sine are more likely to be relevant than lemmas about rings?

[Scott Morrison]

This is why we desperately need a good premise selection engine for Lean. :-(

[Anne Baanen]

Jasmin had a student working on premise selection, let me see if there is anything I can share...

[Scott Morrison]

Great, thank you.

[Scott Morrison]

I think the "requirements" are something like:

• a function that is essentially Expr → List Name, proposing "relevant" lemma names for a goal.
• a downloadable database (presumably <1gb?, and less would be nice?) (but we could survive with a call to a server?)
• that we can arrange for mathlib CI to regenerate on some timetable
• optionally, you can tell it whether you are planning on rewriting and/or applying these lemmas, but one big bucket is fine.
• optionally that provides whatever extra detail, e.g. List (Name × Float) if it wants to expose details of its ranking

A really bad implementation would still be a wonderful contribution, by giving us something to iterate on, and establishing this as a reliably available "component" in the mathlib world.

[Scott Morrison]

In particular, I want something that doesn't try to do more than provide a List Name (i.e. is unopinionated about whether you are throwing these into solve_by_elim, or a search routine, or putting them into the context of an LLM, etc).

[Anne Baanen]

The thesis will be officially made available on https://lean-forward.github.io/ some point in the future. For now, here's the PDF:
Thesis-Alistair-Geesing.pdf and GitHub link for the code: https://github.com/aalistairr/ps-lean

[Scott Morrison]

@Heather Macbeth, when rw? is run with no limits on the number of results, it does find

Try this: rw [← Real.cos_sub_pi_div_two]
-- Real.cos (x - Real.pi / 2) = 1 ↔ ∃ k, x = 2 * Real.pi * ↑k + Real.pi / 2

but currently this is about number 265 in the list... Obviously not very useful.