Zulip Chat Archive

Stream: general

Topic: divides_four


view this post on Zulip Julian Külshammer (Mar 14 2021 at 07:15):

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?

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 08:28):

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

view this post on Zulip Kenny Lau (Mar 14 2021 at 08:30):

you need to revert m and h before doing dec_trivial

view this post on Zulip Julian Külshammer (Mar 14 2021 at 08:56):

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)

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 08:58):

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

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 09:06):

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

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 09:06):

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

view this post on Zulip Julian Külshammer (Mar 14 2021 at 09:09):

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

view this post on Zulip Kenny Lau (Mar 14 2021 at 11:11):

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

view this post on Zulip Kenny Lau (Mar 14 2021 at 11:11):

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

view this post on Zulip Kenny Lau (Mar 14 2021 at 11:12):

because Lean knows that the first hypothesis makes the cases finite

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 12:07):

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

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:20):

there isn't an instance for that

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:21):

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

view this post on Zulip Kevin Buzzard (Mar 14 2021 at 12:24):

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

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:24):

yeah

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:25):

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

view this post on Zulip Julian Külshammer (Mar 16 2021 at 10:08):

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

view this post on Zulip Moritz Firsching (Mar 16 2021 at 22:02):

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?

view this post on Zulip Ruben Van de Velde (Mar 16 2021 at 22:19):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:36):

@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.

view this post on Zulip Damiano Testa (Mar 17 2021 at 06:45):

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)

view this post on Zulip Moritz Firsching (Mar 17 2021 at 08:40):

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


Last updated: May 08 2021 at 10:12 UTC