## Stream: Beginner Questions

### Topic: Simple proof using Decision_Procs/Approximation

#### Heiko Becker (Apr 05 2022 at 07:38):

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?

#### Manuel Eberl (Apr 05 2022 at 07:46):

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.

#### Manuel Eberl (Apr 05 2022 at 07:46):

Someone ought to improve the error message for `approximation` to detect these cases…

#### Manuel Eberl (Apr 05 2022 at 07:47):

I'll put that on my to do list.

#### Heiko Becker (Apr 05 2022 at 07:49):

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?

#### Heiko Becker (Apr 05 2022 at 07:57):

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

#### Manuel Eberl (Apr 05 2022 at 08:37):

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.

#### Manuel Eberl (Apr 05 2022 at 08:38):

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

#### Manuel Eberl (Apr 05 2022 at 08:39):

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

#### Manuel Eberl (Apr 05 2022 at 08:39):

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

#### Manuel Eberl (Apr 05 2022 at 08:40):

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

#### Heiko Becker (Apr 05 2022 at 08:46):

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.

#### Manuel Eberl (Apr 05 2022 at 08:47):

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

#### Manuel Eberl (Apr 05 2022 at 08:47):

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

#### Manuel Eberl (Apr 05 2022 at 08:48):

i.e. that what `approximation` does is simply not good enough

#### Manuel Eberl (Apr 05 2022 at 08:48):

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)

#### Heiko Becker (Apr 05 2022 at 08:49):

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

#### Manuel Eberl (Apr 05 2022 at 09:41):

I cobbled something together for you. My_Experiment.thy

#### Manuel Eberl (Apr 05 2022 at 09:41):

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

#### Manuel Eberl (Apr 05 2022 at 09:42):

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.

#### Manuel Eberl (Apr 05 2022 at 09:42):

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

#### Heiko Becker (Apr 06 2022 at 06:29):

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.

#### Manuel Eberl (Apr 06 2022 at 06:49):

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