Stream: Beginner Questions

Topic: Without loss of generality


view this post on Zulip Chris_Y (Jun 27 2023 at 14:35):

Hi everyone,

My goal is the following:
I can use an existing theorem to show there exist odd positive integers x, y and z such that n = x^2+y^2+z^2 if n mod 8 = 3. However, I'd like to assume without loss of generality that x >= y >= z. This assumption is not given in the original theorem, I wonder if there is any efficient way to do this.

Thank you so much for the help!

view this post on Zulip Manuel Eberl (Jun 27 2023 at 15:09):

The easiest way I see is to rewrite it as n = sum_list (map (λx. x^2) [x,y,z]) and then show that this is the same as sum_list (map (λx. x^2) (sort [x,y,z])) and then obtain values a, b, c such that [a,b,c] = sort [x,y,z].

view this post on Zulip Manuel Eberl (Jun 27 2023 at 15:10):

Each of those steps should be doable with a few suitable library lemmas and help from sledgehammer. But depending on how much experience you have with Isabelle it could still be a bit tricky, so feel free to ask if you are stuck with any particular step.

view this post on Zulip Manuel Eberl (Jun 27 2023 at 15:10):

(might be sensible to go through multisets to justify that the two sets are the same)

view this post on Zulip Manuel Eberl (Jun 27 2023 at 15:11):

alternatively you could of course just do a case distinction; that should also work

view this post on Zulip Manuel Eberl (Jun 27 2023 at 15:12):

That is, proving the stronger version of the theorem from the weaker one with a by (cases "x ≤ y"; cases "y ≤ z"; cases "x ≤ z") (auto simp: algebra_simps) or something like that (not sure if that's enough).

view this post on Zulip Chris_Y (Jun 27 2023 at 16:38):

That works! Thank you so much :)


Last updated: Feb 27 2024 at 08:17 UTC