Ieva Daukantas (Nov 15 2021 at 12:35): 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.
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.
Alessandro Bruni (Nov 15 2021 at 14:13):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: Oct 01 2023 at 18:01 UTC