Quickest way to resolve exponent inequalities

Stream: new members

[Gareth Ma]

Hi, it's me again :P I am working on properties of Mersenne primes i.e. primes in the form of 2^n - 1. One property is that n must be a prime. While working on it, I have to deal with a lot of 2^x, and combined with the subtraction over natural numbers, it is causing me quite a lot of pain :tear: Is that normal? As in, is there any simpler way to prove that 2 <= d => 1 < 2^d - 1 directly, whether through a simp or some other method?

Here is my code, it's all quite elementary number theory, so hope someone can take a look, especially the parts where I marked with TODO, such as stating 4 - 1 <= 2^d - 1 as a lemma. Thanks!!

-- Thank you to Kevin Buzzard, Niels Voss and Yaël Dillies for helping with this!
theorem mersenne_div {m n : ℕ} (h : m ∣ n) : mersenne m ∣ mersenne n :=
begin
  rcases h with ⟨k, rfl⟩,
  simpa only [mersenne, pow_mul, one_pow] using nat_sub_dvd_pow_sub_pow _ 1 _,
end

-- 2^n - 1 is Mersenne prime implies n is prime
theorem mersenne_theorem {n : ℕ} (h : nat.prime (mersenne n)) : nat.prime n :=
begin
  -- Auxillary lemma
  have two_le_n : 2 ≤ n,
  {
    by_contradiction h',
    push_neg at h',

    -- TODO: Simplify this, seems repetitive
    cases nat.lt_succ_iff.1 h' with _ h',
    { simp [mersenne, nat.not_prime_one] at h, exact h, },
    { simp [mersenne, nat.eq_zero_of_le_zero h', nat.not_prime_zero] at h, exact h, }
  },

  -- Assume n is composite
  by_contradiction n_comp,
  rcases nat.exists_dvd_of_not_prime _ n_comp with ⟨d, d_div, d_ne_one, d_ne_n⟩,

  -- TODO: Remove these...
  have d_ne_zero : d ≠ 0,
  { by_contradiction, rw h at d_div, rw zero_dvd_iff at d_div, linarith, },
  have one_le_pow_two_d : 1 ≤ 2 ^ d,
  { apply nat.one_le_pow, omega, },
  have two_le_d : 2 ≤ d,
  { cases d, omega, cases d; omega,},
  have four_sub_one_le_pow_two_sub_one: 4 - 1 ≤ 2 ^ d - 1,
  {
    change 2 ^ 2 - 1 ≤ 2 ^ d - 1,
    rw nat.sub_le_sub_iff_right,
    exact pow_le_pow (by linarith) two_le_d,
    exact nat.one_le_pow d 2 zero_lt_two,
  },

  -- Then mersenne n is not prime
  rcases mersenne_div d_div with ⟨md, hmd⟩,
  have : ¬nat.prime (mersenne n),
  {
    apply nat.not_prime_mul' hmd.symm,
    {
      unfold mersenne,

      -- TODO: Remove this...
      calc
      1 < 4 - 1 : by simp
      ... ≤ 2 ^ d - 1 : by { simp [four_sub_one_le_pow_two_sub_one] },
    },
    {
      -- Ruling out cases where (mersenne n / mersenne d) <= 2
      by_contradiction H,
      push_neg at H,
      cases md,
      { simp [hmd] at h, exact nat.not_prime_zero h, },
      {
        unfold mersenne at hmd,
        rw [nat.succ_le_iff, nat.lt_one_iff] at H,
        simp [H] at hmd,
        -- TODO: Here I am proving 2 ^ n - 1 = 2 ^ d - 1 => n = d ... Is there better way?
        rw [tsub_left_inj (nat.one_le_pow n 2 zero_lt_two) one_le_pow_two_d, eq_comm] at hmd,
        exact d_ne_n (nat.pow_right_injective rfl.ge hmd),
      }
    }
  },

  exact this h,
  exact two_le_n,
end

[Yaël Dillies]

You should probably work over int to use the proper subtraction.

[Yaël Dillies]

Subtraction on nat is very well behaved from the order theoretic point of view, not so much from the algebraic one.

[Gareth Ma]

The thing is mersenne is currently defined as def mersenne (p : ℕ) : ℕ := 2^p - 1, and it is used everywhere in the lucas_* code. Should I change that? Or just cast to the int's and work on that?

[Kevin Buzzard]

Just cast to int and prove mersenne n as integer is 2^n-1 with integer subtraction. Natural subtraction is awful I agree.

[Yaël Dillies]

If that makes you feel better, you could define int.mersenne and show casting nat.mersenne to int gives you int.mersenne.