Hi everyone,

I have been pointed at the Interval library in `Decision_Procs/Approximation`

and I am trying to prove some simple examples with it.

Looking at `Decision_Procs/ex/Approximation_ex`

, a goal like the following should be provable:

```
theory Scratch
imports Complex_Main "HOL-Library.Reflection"
"~~/src/HOL/Decision_Procs/Approximation"
begin
lemma bar:
shows "0 ≤ x ∧ x ≤ 1 ⟹ abs (sin (x)) < 2"
by (approximation 10)
end
```

However, the proof of lemma `bar`

fails with the error ```
Reification failed: Cannot find the atoms equation
Approximation does not support "x ∈ {0..1} ⟶ ¦sin x¦ < 2"
```

Can someone help me understand this error message?

Hah, I can see why that might be confusing. The problem, as is so often the case in Isabelle when something that ought to work doesn't work, is polymorphism.

The way you wrote it down, Isabelle infers the following type for `x`

:

```
'a::{abs,ord,banach,real_normed_algebra_1}
```

You can find that out by doing a `declare [[show_sorts]]`

above your lemma and ctrl+hovering over the `x`

. The `banach`

and `real_normed_algebra_1`

comes from the `sin`

, the `ord`

comes from the `≤`

, and the `abs`

comes from the `abs`

.

If you add an explicit `:: real`

constraint, it works without any problems.

Someone ought to improve the error message for `approximation`

to detect these cases…

I'll put that on my to do list.

Thanks a lot for the explanation! That makes sense. I will add that explicitly. HOL4 does support something along the lines of `realsLib.prefer_reals()`

which tells the parser to disambiguate into reals as much as possible. Is there maybe something similar for Isabelle?/HOL?

One more question: I was pointed at the `approximation`

work by a reviewer whom suggested to look into it for polynomial inequalities. I am now trying a very simple goal from our evaluation, and the only error I get is `Failed to apply initial proof method⌂:[...]`

when using `apply (approximation 30)`

on this goal

```
lemma foo:
assumes "(0 ≤ x ∧ x <= 2/5)"
shows "(abs(cos (x) - (50000000135927169520044799355673603713512420654297 /
50000000000000000000000000000000000000000000000000 +
(x *
(-1225409217893488553021618054153507593184713186929 /
2500000000000000000000000000000000000000000000000000000) +
(x * x *
(-24999283897945898114123508548800600692629814147949 /
50000000000000000000000000000000000000000000000000) +
(x * x * x *
(-3061900846609820763151443845373478325200267136097 /
20000000000000000000000000000000000000000000000000000) +
(x * x * x * x *
(21203466323626414535841178121700068004429340362549 /
500000000000000000000000000000000000000000000000000) +
x * x * x * x * x *
(-16524268822046756562821334668456074723508208990097 /
10000000000000000000000000000000000000000000000000000))))))):: real)
<=
19552407163238115144356799930793053619830587160513/5000000000000000000000000000000000000000000000000000000000"
```

That usually indicates that `approximation`

wasn't able to verify the statement, either because it is false or because the precision wasn't high enough.

(Or because there is a completeness bug in the code)

But you shouldn't forget to chain in the assumption here.

i.e. `using assms by (approximation …)`

I think it may also help to cut the interval a bit more

Ok, thanks for the explanations. I will try with `using assms`

again and see what happens. We used CoqInterval on those examples too where we needed bisections and taylor models. I will experiment with the parameters to `approximation`

a bit then.

It does support Taylor stuff and bisections, have a look at the examples in the `HOL/Decision_Procs/ex`

directory.

but I wasn't able to get this one through, so it's possible that there is some problem there

i.e. that what `approximation`

does is simply not good enough

there are Taylor Models in Isabelle as well; Fabian Immler will be able to help you with those (though he works at Apple now; not sure if he will reply)

Thanks a lot for all of the help. I will keep experimenting with it.

I cobbled something together for you. My_Experiment.thy

Unless I messed something while copy-pasting, this verifies that your inequality holds using Taylor models, within about 1.7 seconds in my machine.

It's a bit messy because Fabian never seems to have done the same kind of nice reification that exists for `approximation`

and the interface to the Taylor Model library is a bit unpolished, but I think I figured out how to set it up correctly.

You might want to run this by Fabian for a comment though.

Thank you very much for the file. I will look at it carefully. I will first check whether I can automatically generate inputs of the form described in the file before I start bugging more people.

I mean you could contact him about what this `prove_pos`

thing actually does and whether there is a correctness proof

Last updated: Sep 25 2022 at 23:25 UTC