Craig Alan Feinstein (Jul 29 2024 at 03:56): Craig Alan Feinstein (Jul 29 2024 at 03:56):Chelsea Edmonds pointed out to me the is_square function. I tried using it with no luck in the show ?thesis line. Any ideas? I would think this would prove (๐ - ฮ)^(๐ - 1) to be a square. Do I need to do more, like prove that det N / k is rational or natural?
proof -
have "(det N / ๐)^2 = (๐ - ฮ)^(๐ - 1)"
using power_of_k_minus_lambda_2 by simp
then show ?thesis by try0
?
One of my goals is to prove in Isabelle that is sqrt x is rational and x is natural then sqrt x is natural. Iโm having trouble with this seemingly simple goal.
Chelsea Edmonds (Jul 29 2024 at 09:34):Craig Alan Feinstein said:
Chelsea Edmonds pointed out to me the is_square function. I tried using it with no luck in the show ?thesis line. Any ideas? I would think this would prove (๐ - ฮ)^(๐ - 1) to be a square. Do I need to do more, like prove that det N / k is rational or natural?
proof - have "(det N / ๐)^2 = (๐ - ฮ)^(๐ - 1)" using power_of_k_minus_lambda_2 by simp then show ?thesis by try0 ?
Try using "unfolding is_square_def" next to thesis, or (simp add: is_square_def) and see what the new proof goals are. Those proof goals should then guide your proof. This is a good starting point when working with any definition.
Chelsea Edmonds (Jul 29 2024 at 09:38):Craig Alan Feinstein said:
One of my goals is to prove in Isabelle that is sqrt x is rational and x is natural then sqrt x is natural. Iโm having trouble with this seemingly simple goal.
From memory of the paper proof you showed me, I don't think it uses sqrts, and I'm pretty sure you won't need it in Isabelle either. Think the other way, i.e. can you find a number, such that if you square it, it is equal to x.
Craig Alan Feinstein (Jul 29 2024 at 16:19):@Chelsea Edmonds when I tried both "unfolding is_square_def" and "(simp add: is_square_def" I got "Undefined fact: "is_square_def""
Craig Alan Feinstein (Jul 29 2024 at 16:21):@Chelsea Edmonds the goal of proving that sqrt x is rational and x is natural implies sqrt x is natural is a side goal that doesn't necessarily impact the proof. I just wanted to see how to do it.
Chelsea Edmonds (Jul 29 2024 at 16:21):Craig Alan Feinstein said:
Chelsea Edmonds when I tried both "unfolding is_square_def" and "(simp add: is_square_def" I got "Undefined fact: "is_square_def""
That typically means it's an abbreviation. Go and look at where is_square is defined (cntr+click, or search for it), and then try the same things with the definition in the abbreviation.
Craig Alan Feinstein (Jul 29 2024 at 16:33):@Chelsea Edmonds Ok, I did that and got when I hovered over "is_square"ย :
free variable
:: 'a โ bool
Craig Alan Feinstein said:
Chelsea Edmonds Ok, I did that and got when I hovered over "is_square"ย :
free variable :: 'a โ bool
Ok, so as previously mentioned, if text is blue that means the definition isn't recognised in your current context and will usually be a free variable if you hover over it. Have you imported "HOL-Computational_Algebra.Nth_Powers" (was in my email reply).
Craig Alan Feinstein (Jul 29 2024 at 16:47):Yes, "HOL-Computational_Algebra.Nth_Powers" was imported.
Chelsea Edmonds (Jul 29 2024 at 16:55):Craig Alan Feinstein said:
Yes, "HOL-Computational_Algebra.Nth_Powers" was imported.
That's bizarre, it should definitely be recognised and was recognised for me. Maybe check the import is working properly (i.e. can you click on that file and find is_square yourself in it). Otherwise maybe something else in your theory is messing it up? Try moving the theorem statement to the top of the file and see if it becomes defined maybe, otherwise I don't know what's going on sorry!
Edit, just double checking you're talking about it saying that when you hover over it in your own file? Worth noting just in case, wherever the abbreviation is defined in the Nth_Powers theory it will also say that when you hover over it , but at that point you should be looking at the right side of the definition (i.e. see it uses is_nth_power, so try applying unfolding is_nth_power instead in your own proof). If it's not defined in your own file though, above still applies!
Craig Alan Feinstein (Jul 29 2024 at 22:04):I meant when I hover over it in the hol computational algebra file with powers definitions. When I press cntl and click over is_square in my file I get led to that hol file.
Craig Alan Feinstein (Jul 30 2024 at 01:53):I'm going to concentrate on the difficult part of the BRC proof now for odd v. proving that sqrt(k-lambda) is an integer follows relatively from sqrt(k-lambda) being a rational, which I already proved. It would be good to have such a lemma in Isabelle.
Chelsea Edmonds (Jul 30 2024 at 10:24):Craig Alan Feinstein said:
I meant when I hover over it in the hol computational algebra file with powers definitions. When I press cntl and click over is_square in my file I get led to that hol file.
Great, then there's no issue - just no reason to hover over is_square where the abbreviation is being set up! Once you've found where something is defined, looking at what is on the right side of the equality (which I hinted at above) should give you an idea of what definition you need to unfold.
Chelsea Edmonds (Jul 30 2024 at 10:27):Craig Alan Feinstein said:
I'm going to concentrate on the difficult part of the BRC proof now for odd v. proving that sqrt(k-lambda) is an integer follows relatively from sqrt(k-lambda) being a rational, which I already proved. It would be good to have such a lemma in Isabelle.
It exists in several forms. Try using a search tool like FindFacts (https://search.isabelle.in.tum.de/#) or Serapis (https://behemoth.cl.cam.ac.uk/search/) and you should be able to find a few versions of it (e.g. nonneg_sqrt_nat_or_irrat)
Craig Alan Feinstein (Jul 31 2024 at 02:47):@Chelsea Edmonds I can see those two libraries being helpful. I found the lemma I was looking for. I now have finished proving the even part of the BRC. Thanks again.
Last updated: Dec 21 2024 at 16:20 UTC