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`

is this `nat`

or `Z`

or `Q`

? `sqrt`

definition is different for them. I also don't see what `(/ ...)`

could mean.

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.

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

for reals you can try Gappa and interval

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

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.

Thank you for the help.

Fantastic!

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: Jun 25 2024 at 15:02 UTC