Stream: Beginner Questions

Topic: sqrt

zibo yang (Apr 22 2021 at 16:31):

Hi, is there any lemma or theorem in HOL library like: "a>=0 --> b>=0 --> sqrt(a * b) =sqrt(a) *sqrt(B)"

Mathias Fleury (Apr 22 2021 at 16:33):

Have you tried to search for it?

Jakub Kądziołka (Apr 22 2021 at 16:34):

the query "sqrt (?a * ?b)" finds the relevant theorem

Mathias Fleury (Apr 22 2021 at 16:34):

The standard ways are:

find_theorems "sqrt (?a * ?b) = sqrt ?a * sqrt ?b"

or

 sledgehammer
(*and looking at the used facts*)

zibo yang (Apr 22 2021 at 16:36):

thanks a lot. I get some clues

Mathias Fleury (Apr 22 2021 at 16:38):

BTW, your lemma should be

 a>=0 ==> b>=0 ==> sqrt(a * b) =sqrt(a) *sqrt(B)

with meta-implication instead of HOL implications

zibo yang (Apr 22 2021 at 16:38):

another stupid question: is "r ^ 2" the right form to type when expressing the square of r

Jakub Kądziołka (Apr 22 2021 at 16:51):

yeah

Jakub Kądziołka (Apr 22 2021 at 16:51):

if you want to unfold it into r * r later, use power2_eq_square

zibo yang (Apr 22 2021 at 16:55):

ok.I got it

Last updated: Dec 21 2024 at 16:20 UTC