Stream: Coq users

Topic: Computing with reals and sqrt


view this post on Zulip Ieva Daukantas (Nov 15 2021 at 12:35):

What would be the best way to prove this goal?
1 / 16 + 2 * (1 / 12) * (/ (4 * sqrt (2 - 1 / 12)) + / sqrt (1 - 1 / 12))² <= 0.32

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:39):

is this nat or Z or Q? sqrt definition is different for them. I also don't see what (/ ...) could mean.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:40):

for some encodings, you could probably just do vm_compute and get an answer fast. If there are non-ground symbols, I'd take a look at Micromega tactics, possibly augmented with some lemma about the sqrt you end up using.

view this post on Zulip Ieva Daukantas (Nov 15 2021 at 12:44):

Hi Karl, thanks. It is about Reals and nra does not seem to work.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:49):

for reals you can try Gappa and interval

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:57):

Require Import Reals Interval.Tactic.
Open Scope R_scope.
Goal 1 / 16 + 2 * (1 / 12) * (/ (4 * sqrt (2 - 1 / 12)) + / sqrt (1 - 1 / 12))² <= 0.32.
interval.
Qed.

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:57):

For this goal Interval is the tool of choice. Gappa is for proving deviations between a real term and exactly the same term evaluated with float or fixed point arithmetic. coq-interval is very powerful and can substantially more complicated things. It is also quite fast.

view this post on Zulip Ieva Daukantas (Nov 15 2021 at 12:59):

Thank you for the help.

view this post on Zulip Alessandro Bruni (Nov 15 2021 at 14:13):

Fantastic!

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:14):

if you actually want to compute with your reals (as opposed to using tactics), I'd recommend looking at https://github.com/coq-community/corn - keyphrase "Exact Real Computation" (but probably not an easy fit)


Last updated: Feb 04 2023 at 21:02 UTC