mod and lt

Stream: maths

[Matthew Pocock]

I'm getting a bit muddled trying to reason about lt inequalities.

theorem t1 (n: Nat) : 0 < n → 0 < 2*n := by
    simp

theorem t2 (n: Nat) : n % 2 = 0 →  0 < n / 2 → 0 < n := by
    intro m2
    have a2 : n = 2*a := by
        -- n % 2 = 0 -> n = 2*a
        admit
    rw [a2]
    simp

It all works out in t1, but in t2 it can't see through the division by 2. Multiplying through by 2 lets it simplify again. I was going to make use of the knowledge that n is even to rewrite it into a form with the factor of 2 in it, but when I try this, I keep introducing a new top-level variable to the theorem. I really just want a temporary or private variable. And I can't seem to find a rule involving mod that lets me do the rewrite anyway.

I wasn't sure if this was a maths question or a general one.

[Damiano Testa]

Does have a2 : ∃ a, n = 2 * a := by exact? yield anything useful?

[Matthew Pocock]

Damiano Testa said:

Does have a2 : ∃ a, n = 2 * a := by exact? yield anything useful?

The exact? tactic isn't closing that have, and the resulting a2 with the existential doesn't seem to let me make any progress

[Damiano Testa]

Assuming the ∃, you can do cases a2 to "open up the existential".

[Damiano Testa]

To prove the existential, you may have to convert the % into a divisibility statement, something like mod_eq_zero_iff_dvd (guessing here...).

[Matthew Pocock]

theorem modlt1 (n: Nat) : n % 2 = 0 →  0 < n / 2 → 0 < n := by
    intro m2
    have a2 : ∀ a, n = 2 * a := (λ a ↦ n = 2 * a)
    rw [a2]
    simp
    use 1

The universal allows it to work where the existential doesn't. If I replace everything after := with sorry, it accepts the proof. However, it won't let me build a2 from that lambda.

[Ruben Van de Velde]

That universal makes no mathematical sense: n can't be equal to 2a for all a

[Ruben Van de Velde]

Changing to a divisibility statement does indeed help:

theorem modlt1 (n: Nat) : n % 2 = 0 →  0 < n / 2 → 0 < n := by
  intro m2
  obtain ⟨k, rfl⟩ := dvd_of_mod_eq_zero m2
  simp

[Matthew Pocock]

Ruben Van de Velde said:

Changing to a divisibility statement does indeed help:

Thanks. dvd_of_mod_eq_zero was exactly what I needed. Is there a way to search for all theorems that can act on some hypothesis? Or do I just need to memorise more of the library?

[Ruben Van de Velde]

In this case, rw? at m2 finds the iff version for me

[Ruben Van de Velde]

However, I found it by guessing there would be a relevant theorem with mod_eq_zero in the name - because that's how things are named in mathlib. So I started typing that and used ctrl+space in vscode to bring up autocompletion suggestions, and I found it there