## Stream: Coq users

### Topic: Computing with reals and sqrt

#### 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`

#### 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.

#### 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.

#### Ieva Daukantas (Nov 15 2021 at 12:44):

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

#### Karl Palmskog (Nov 15 2021 at 12:49):

for reals you can try Gappa and interval

#### 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.
``````

#### 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.

#### Ieva Daukantas (Nov 15 2021 at 12:59):

Thank you for the help.

Fantastic!

#### 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