divides_four

Stream: general

[Julian Külshammer]

I'm in the process of showing that a particular element of a (generalised) quaternion group has order 4. It is of course easy to show that the order divides four by just checking that the element to the power of 4 is equal to one. I'd now like to deduce that it is equal to 4 by showing that it is not 1 or 2 (which should be straightforward). I would use the following (but feel free to suggest a better strategy:

import data.nat.basic

example (m : ℕ) (h : m ∣ 4) : m = 1 ∨ m = 2 ∨ m = 4 := sorry

What is an easy way to prove this?

[Kevin Buzzard]

Does dec_trivial do it? If not I'd be tempted to prove it's <= 4 using the library and then use the natural case bash tactic interval_cases

[Kenny Lau]

you need to revert m and h before doing dec_trivial

[Julian Külshammer]

revert h, revert m, dec_trivial gives the error failed to synthesize type class instance for decidable (∀ (m : ℕ), m ∣ 4 → m = 1 ∨ m = 2 ∨ m = 4)

[Kevin Buzzard]

Hard luck. The correct thing to do is to show that dvd is decidable and/or fill in the hole in the library that is stopping Lean from figuring out it's decidable. Or just go with the case bash

[Kevin Buzzard]

import tactic

example (m : ℕ) (h : m ∣ 4) : m = 1 ∨ m = 2 ∨ m = 4 :=
begin
  have h2 : m ≤ 4 := nat.le_of_dvd (by norm_num) h,
  interval_cases m; clear h2,
  { finish },
  { cc },
  { cc },
  { exfalso,
    -- prove 3 doesn't divide 4 somehow
    sorry },
  { cc }
end

[Kevin Buzzard]

Lean is not a very good "computer" right now because we didn't put much effort into doing explicit calculations.

[Julian Külshammer]

Ok, I'll do interval_cases then for now. Thanks for the input Kenny and Kevin.

[Kenny Lau]

import tactic

example (m : ℕ) (h : m ∣ 4) : m = 1 ∨ m = 2 ∨ m = 4 :=
begin
  have := nat.le_of_dvd dec_trivial h,
  revert h,
  revert this,
  revert m,
  exact dec_trivial
end

[Kenny Lau]

∀ (m : ℕ), m ≤ 4 → m ∣ 4 → m = 1 ∨ m = 2 ∨ m = 4 is decidable

[Kenny Lau]

because Lean knows that the first hypothesis makes the cases finite

[Kevin Buzzard]

But shouldn't lean know that m dvd succ 3 makes the cases finite?

[Mario Carneiro]

there isn't an instance for that

[Mario Carneiro]

lean knows that \forall x, x <= n -> P x is decidable if P is, and there is a lemma that says x | n -> x <= n, but those two are not combined to an instance that says \forall x, x | n -> P x is decidable if P is

[Kevin Buzzard]

So if this instance is added then the proof is revert-everything; dec_trivial?

[Mario Carneiro]

yeah

[Mario Carneiro]

although adding instances like this is a can of worms; there are a whole lot of predicates that imply x is bounded

[Julian Külshammer]

Just to report back that in the PR process, @Scott Morrison had the wonderful suggestion of using nat.eq_prime_pow_of_dvd_least_prime_pow to prove the following lemma first and then apply it in the situation of the quaternion group.

lemma order_of_eq_prime_pow {a : α} {p k : ℕ} :
nat.prime p → (¬ a ^ p ^ k = 1) → (a ^ p ^ (k + 1) = 1) → order_of a = p ^ (k + 1) :=
begin
  intros hprime hnot hfin,
  apply nat.eq_prime_pow_of_dvd_least_prime_pow hprime,
    { rw order_of_dvd_iff_pow_eq_one,
      exact hnot },
    { rw order_of_dvd_iff_pow_eq_one,
      exact hfin },
end

[Moritz Firsching]

golf:

lemma order_of_eq_prime_pow {a : α} {p k : ℕ} :
nat.prime p → (¬ a ^ p ^ k = 1) → (a ^ p ^ (k + 1) = 1) → order_of a = p ^ (k + 1) :=
begin
  intros hprime hnot hfin,
  apply nat.eq_prime_pow_of_dvd_least_prime_pow hprime,
    { rwa order_of_dvd_iff_pow_eq_one, },
    { exact order_of_dvd_of_pow_eq_one hfin, },
end

Actually I'm not quite sure what the goals for golfing lean is. What are we optimizing for? The number of characters in the proof? The time it takes to build the proof? The length of what is shown by show_term?

[Ruben Van de Velde]

If the lemma is mathematically trivial, there tends to be a focus on making the proof as short as possible. In this case, your proof is fine, I think. I might move the hypotheses to the left of the colon, though:

lemma order_of_eq_prime_pow {a : α} {p k : ℕ}
(hprime : nat.prime p) (hnot : ¬ a ^ p ^ k = 1) (hfin : a ^ p ^ (k + 1) = 1) : order_of a = p ^ (k + 1) :=
begin
  apply nat.eq_prime_pow_of_dvd_least_prime_pow hprime,
  { rwa order_of_dvd_iff_pow_eq_one, },
  { exact order_of_dvd_of_pow_eq_one hfin, },
end

[Johan Commelin]

@Moritz Firsching Like Ruben said, if the statement is so trivial that you don't care what the proof looks like, the proof might as well be short (in the sense of characters), but if by super_heavy_hammer proves the lemma, but takes 3 minutes to do so, then we might want a slightly longer proof that is also fast.

[Damiano Testa]

Here is a further golfing:

lemma order_of_eq_prime_pow {a : α} {p k : ℕ} (hprime : nat.prime p)
  (hnot : ¬ a ^ p ^ k = 1) (hfin : a ^ p ^ (k + 1) = 1) : order_of a = p ^ (k + 1) :=
nat.eq_prime_pow_of_dvd_least_prime_pow hprime (λ h, hnot (order_of_dvd_iff_pow_eq_one.mp h))
  (order_of_dvd_iff_pow_eq_one.mpr hfin)

[Moritz Firsching]

Thanks for the explanation about golfing, @Johan Commelin ; I think I got the idea.