Stream: Beginner Questions

Topic: sqrt


view this post on Zulip 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)"

view this post on Zulip Mathias Fleury (Apr 22 2021 at 16:33):

Have you tried to search for it?

view this post on Zulip Jakub Kądziołka (Apr 22 2021 at 16:34):

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

view this post on Zulip 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*)

view this post on Zulip zibo yang (Apr 22 2021 at 16:36):

thanks a lot. I get some clues

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Apr 22 2021 at 16:51):

yeah

view this post on Zulip Jakub Kądziołka (Apr 22 2021 at 16:51):

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

view this post on Zulip zibo yang (Apr 22 2021 at 16:55):

ok.I got it


Last updated: Sep 25 2021 at 08:21 UTC