Stream: general

Topic: divides_four

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?

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

Kenny Lau (Mar 14 2021 at 08:30):

you need to revert m and h before doing dec_trivial

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)

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

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


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.

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.

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


Kenny Lau (Mar 14 2021 at 11:11):

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

Kenny Lau (Mar 14 2021 at 11:12):

because Lean knows that the first hypothesis makes the cases finite

Kevin Buzzard (Mar 14 2021 at 12:07):

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

Mario Carneiro (Mar 14 2021 at 12:20):

there isn't an instance for that

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

Kevin Buzzard (Mar 14 2021 at 12:24):

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

yeah

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

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


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?

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


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.

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)


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