Greatest multiple less or equal to number

Stream: new members

[Markus Schmaus]

I want to compute the greatest multiple of n less or equal to m. And I find it surprisingly hard to proof the correctness of the result.

def greatestMultiple (n m : Nat) : Nat := m - (m % n)

theorem greatestMultipleLt_greatest (n m : Nat) :
    ∀ k ≤ m, n ∣ k → k ≤ greatestMultiple n m := by
  sorry

Is there an easy proof for this?

[Markus Himmel]

Here's one way:

theorem greatestMultipleLt_greatest (n m : Nat) :
    ∀ k ≤ m, n ∣ k → k ≤ greatestMultiple n m := by
  rintro k hk h
  rw [← Nat.mul_div_cancel' h, greatestMultiple, ← Nat.mul_div_cancel' (Nat.dvd_sub_mod m),
    ← Nat.div_eq_sub_mod_div]
  apply Nat.mul_le_mul_left
  exact Nat.div_le_div_right hk

[Markus Schmaus]

Thank you. I think I underestimated the power of rw (opting for simp most of the time).

Is there any trick how you found the relevent theorems? Did you just use loogle?

[Markus Himmel]

I used a combination of Loogle, typing things like Nat.div_le and seeing what autocomplete suggests, and scrolling around in the div section of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Defs.html

[Ralf Stephan]

You know grep?. I found grep -ri 'theorem.*some pattern' .lake/packages/mathlib/Mathlib |less quite effective.

[Kevin Buzzard]

Are there times when this is more powerful than just using the API docs and searching there?

[Ruben Van de Velde]

One advantage might be that it's on your own machine

[Damiano Testa]

I often combine this with grep regexes, as well.

[Ralf Stephan]

Kevin Buzzard said:

Are there times when this is more powerful than just using the API docs and searching there?

For example, when you want context right away, instead of clicking on "source" in the API docs, then use grep with the -C option, like grep -ir -C3 ....

[Ralf Stephan]

Also, how would you find without grep where a specific theorem is used?

[Yaël Dillies]

This specific information is stored in the .ilean files, so you could query it from within Lean. Try eg to click F2 on a declaration's name and rename it to foo. You will see that all occurrences within the library have been rewritten.