Trouble making proof of Archimedean_Property more effcient

Stream: new members

[Ibrahim Sufi]

Hi,
I am Ibrahim. I am an undergraduate at the University of Kansas. I am new to Lean. I am trying to prove the Archimedean Property of the positive integers and I was able to prove it but the proof is really long and I know there are ways to do it in less steps. I was was wondering if anyone had any suggestions. Here is my code. Thanks.

import Mathlib.Algebra.Order.Ring.Defs
import Mathlib.Tactic.Cases
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
open Classical

theorem archimedean_property_by_well_ordering (a b : ℤ) (ha: 0 ≤ a) (hb : b > 0) : ∃ (n : ℕ), n * b > a := by
  let differences : ℕ  → Prop := fun y => ∃ n ≥ 0, y = a - b * n
  have : DecidablePred differences := fun n => by simp [differences]; infer_instance
  have h: ∃ y, differences y := by
    use Int.toNat a
    simp [differences]
    use 0
    apply And.intro
    trivial
    simp only [mul_zero, sub_zero]
    apply Int.max_eq_left ha


  let y := Nat.find h
  have h2 : ∃ n ≥ 0, y = a - b*n := by
    exact Nat.find_spec h

  cases h2 with
    | intro n pn =>
      use Int.toNat (n + 1)
      contrapose! pn
      intro greater
      intro h3
      have h4 : y - b ≥ 0 := by
        have greater2: n + 1 ≥ 0 := by
          linarith
        rw [Int.toNat_of_nonneg greater2] at pn
        linarith
      have h5 : differences (Int.toNat (y - b) ) := by
        simp [differences, Int.toNat_of_nonneg h4]
        use n + 1
        apply And.intro
        linarith
        linarith
      have h6 (m: ℕ ) : m < y → ¬ differences m := by
        exact Nat.find_min h
      have h7 : y - b < y := by
        linarith
      rw [← Int.toNat_of_nonneg h4] at h7
      rw[Int.ofNat_lt] at h7
      apply h6 at h7
      trivial

[Matt Diamond]

Could you include your imports as well? Click #mwe for more information.

[Ibrahim Sufi]

Matt Diamond said:

Could you include your imports as well? Click #mwe for more information.

Sorry just added them.

[Matt Diamond]

one small thing I would suggest is to write inequalities as < or ≤ instead of > or ≥, as mathlib is somewhat standardized around less-than (the majority of inequalities in mathlib lemmas are written that way)

so you might want to write the statement as:

theorem archimedean_property_by_well_ordering (a b : ℤ) (ha: 0 ≤ a) (hb : 0 < b) : ∃ (n : ℕ), a < n * b := sorry

[Matt Diamond]

I don't know if this helps, but here's a (very) short proof:

import Mathlib

theorem archimedean_property (a b : ℤ) (hb : 0 < b) : ∃ (n : ℕ), a < n * b :=
⟨Nat.ceil ((a / b) + 1), Int.lt_mul_of_ediv_lt hb (by simp)⟩

[Matt Diamond]

(maybe a bit too short...)

[Ibrahim Sufi]

I am trying to re derive a lot of the results from basic number theory. So I think I wanted to start with the well ordering principle because I haven't proved the division algorithm yet.

[Matt Diamond]

another minor stylistic point: you can remove the have : DecidablePred differences line... since you're working in classical mode, it's assumed that all predicates are decidable