Square root function · Beginner Questions

Stream: Beginner Questions

Topic: Square root function

Tingyou PAN (Jun 09 2024 at 10:11):

I am trying to use the square root function in Isabelle. For example, I wrote the following

theory square_root_example
imports Main HOL.Real
begin

value "sqrt (4::real)"

end

However, the output for the line starting with "value" is

:: "'a"

indicating that the function represented by "sqrt" is not defined. After searching the web, I found the sqrt function only needed the libraries "HOL.Real" and "Main", which strangely do not work in my case. I am using Isabelle 2023 for MacOS. What should I import in order to use the "sqrt" function?

Yong Kiam (Jun 09 2024 at 13:05):

HOL-Analysis.Analysis should work but might be too much

Tingyou PAN (Jun 09 2024 at 14:33):

Yong Kiam said:

HOL-Analysis.Analysis should work but might be too much

Thank you for your suggestions. Unfortunately, after I imported the files, which took about ten minutes to verify on my computer, I still couldn't use the "sqrt" function. This time, when I entered

value "sqrt (4::real)"

the output was something related to wellsortedness error. Is there some other ways that I can use this function? Thanks again for your help.

Mathias Fleury (Jun 09 2024 at 14:37):

what do you expect? And what do you expect for sqrt 2?

Mathias Fleury (Jun 09 2024 at 14:40):

Because if you are only interested in perfect squares the solution will be different from let's say an algorithm to compute an approximation

Tingyou PAN (Jun 09 2024 at 14:41):

Mathias Fleury said:

what do you expect? And what do you expect for sqrt 2?

For example, for

value "sqrt (4::real)"

I was expecting something like 2. As for sqrt 2, perhaps something without error messages. I am trying to prove something related to square roots of arbitrary positive real numbers.

Yong Kiam (Jun 09 2024 at 14:44):

regarding your 10minutes-to-verify problem, I would suggest restarting Isabelle with -l HOL-Analysis to create the appropriate heap so that next time you load it up it'll be fsater

Mathias Fleury (Jun 09 2024 at 14:53):

Tingyou PAN said:

Mathias Fleury said:

what do you expect? And what do you expect for sqrt 2?

For example, for
value "sqrt (4::real)"
I was expecting something like 2. As for sqrt 2, perhaps something without error messages. I am trying to prove something related to square roots of arbitrary positive real numbers.

I don't think that this is possible with the code generator.

Tingyou PAN (Jun 09 2024 at 14:53):

Yong Kiam said:

regarding your 10minutes-to-verify problem, I would suggest restarting Isabelle with -l HOL-Analysis to create the appropriate heap so that next time you load it up it'll be fsater

Thanks, I will definitely try this.

Tingyou PAN (Jun 09 2024 at 14:56):

Is it possible though, if I just want to use the sqrt function to verify trivial things like "sqrt 2 + sqrt 3 < 4"? I saw some similar simple examples on the Internet, but they all seem to only import "HOL.Real".

Yong Kiam (Jun 09 2024 at 15:00):

something concrete like this should be doable using the approximation tactics automatically

Mathias Fleury (Jun 09 2024 at 15:07):

theory Scratch
  imports "HOL-Decision_Procs.Approximation"
begin

approximate "sqrt 2 + sqrt 3 - 5"
(*
"{- 1853735634 / 10 ^ 9..- 1853735629 / 10 ^ 9}"
  :: "real set"
*)

Mathias Fleury (Jun 09 2024 at 15:08):

I am not sure how to generate a theorem out of it

Mathias Fleury (Jun 09 2024 at 15:08):

but I also spent around 1min scrolling through the Approximation file

Yong Kiam (Jun 09 2024 at 15:08):

state the inequality then approximation X where X is a precision parameter

Tingyou PAN (Jun 09 2024 at 15:11):

Thank you very much for this example using approximation! I guess I will stick to this method for now.

Wenda Li (Jun 10 2024 at 09:28):

For a more exact approach, you can perhaps check Rene Thiemann's field extensions of the form Q[sqrt(b)], which enables us to do the following evaluations:

value "⌊101.1 * (sqrt 18 + 6 * sqrt 0.5)⌋"
value "⌊324 * sqrt 7 + 0.001⌋"
value "101.1 * (sqrt 18 + 6 * sqrt 0.5) = 324 * sqrt 7 + 0.001"
value "101.1 * (sqrt 18 + 6 * sqrt 0.5) > 324 * sqrt 7 + 0.001"
value "show (101.1 * (sqrt 18 + 6 * sqrt 0.5))"
value "(sqrt 0.1 ∈ ℚ, sqrt (- 0.09) ∈ ℚ)"

As an overkill, you may even want to check the Algebraic Numbers entry, which allows us to do symbolic calculation using algebraic numbers (like in modern computer algebra systems).

Tingyou PAN (Jun 10 2024 at 15:01):

Wenda Li said:

For a more exact approach, you can perhaps check Rene Thiemann's field extensions of the form Q[sqrt(b)], which enables us to do the following evaluations:
value "⌊101.1 * (sqrt 18 + 6 * sqrt 0.5)⌋"
value "⌊324 * sqrt 7 + 0.001⌋"
value "101.1 * (sqrt 18 + 6 * sqrt 0.5) = 324 * sqrt 7 + 0.001"
value "101.1 * (sqrt 18 + 6 * sqrt 0.5) > 324 * sqrt 7 + 0.001"
value "show (101.1 * (sqrt 18 + 6 * sqrt 0.5))"
value "(sqrt 0.1 ∈ ℚ, sqrt (- 0.09) ∈ ℚ)"
As an overkill, you may even want to check the Algebraic Numbers entry, which allows us to do symbolic calculation using algebraic numbers (like in modern computer algebra systems).

Seems really interesting! They might be a bit advanced for me, but I found it really helpful. Thank you very much for these!

Last updated: Dec 21 2024 at 16:20 UTC