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: Dec 21 2024 at 16:20 UTC