Email Gateway (Aug 22 2022 at 14:31): Email Gateway (Aug 22 2022 at 14:31):From: noam neer <noamneer@gmail.com>
hi everybody.
I'm interested in what exactly happens in the following proof -
theory tmp
imports Complex_Main
begin
lemma "sin((x::real) + y + x) = sin(2*x + y)"
using [[simp_trace=true]]
by simp
end
the proof succeeds, and because of the sin() I guess it can't be due to
linarith.
so I guess there is a true rewriting process here, but I failed to
understand
from the output what exactly happens and how the following expression
appeared
in the process -
(Numeral1 / Numeral1 + Numeral1 / Numeral1) * (x / 1) + y = 2 /
Numeral1 * (x / 1) + (y + 0)
where did all the numerals come from? I expect a rewriting process to
remove things
like Numerla1, not add them.
thanx, Noam
Email Gateway (Aug 22 2022 at 14:31):From: Tobias Nipkow <nipkow@in.tum.de>
On 04/11/2016 04:53, noam neer wrote:
hi everybody.
I'm interested in what exactly happens in the following proof -theory tmp
imports Complex_Main
begin
lemma "sin((x::real) + y + x) = sin(2*x + y)"
using [[simp_trace=true]]
by simp
endthe proof succeeds, and because of the sin() I guess it can't be due to
linarith.
so I guess there is a true rewriting process here, but I failed to
understand
from the output what exactly happens and how the following expression
appeared
in the process -(Numeral1 / Numeral1 + Numeral1 / Numeral1) * (x / 1) + y = 2 /
Numeral1 * (x / 1) + (y + 0)
This is a step in the process that rewrites x+y+x to 2*x+y. As it says in the trace:
Procedure "Numeral_Simprocs.field_combine_numerals" produced rewrite rule:
x + y + x ≡ 2 * x + y
In the next step in the trace, the goal is solved by reflexivity.
Numeral1 is introduced locally by the proof method that combines summands.
Tobias
where did all the numerals come from? I expect a rewriting process to
remove things
like Numerla1, not add them.thanx, Noam
Email Gateway (Aug 22 2022 at 14:33):From: noam neer <noamneer@gmail.com>
first I must admit I didn't know the simplifier can do things to sub
expressions besides application of identities. good to know that.
second, is there a documentation of what "field_combine_numerals" can and
can't do? for example to my surprise the following fails (and this was the
trigger to the original question) -
lemma "sin((x::real) + y + x + y) = sin(2x + 2y)"
using [[simp_trace=true]]
by simp (* doesn't work *)
also, I must say that the simplifier's output is very hard to read. it
would have been much easier to understand it if there was some identation,
and if there was some declaration where the output of a simproc begins (I
assume much of the output before the produced rewrite rule also came from
the simproc.) can we request this for the next Isabelle revision ?
many thanks,
Noam
Email Gateway (Aug 22 2022 at 14:33):From: Lawrence Paulson <lp15@cam.ac.uk>
In such situations, you should try simplifying with
apply (simp add: algebra_simps)
It works in your example. Sledgehammer also solves your problem.
There are many other useful packages of rules for such situations, including field_simps and divide_simps.
To be quite honest, I never try to trace the simplifier. The output is simply too massive. I just try something else.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:33):From: noam neer <noamneer@gmail.com>
hi,
I just experimented with sledgehammer for the first time.
it seems quite impressive, but also a little unstable.
sometimes it doesn't return any output, sometimes I get messages like
"z3": Timed out.
(and four more lines like this)
and sometimes it does return a useful command.
so it seems I always have to try it several times.
is there a way to make it more stable?
I'm using the default installation of Isabelle 2015 on win7.
also, I bring here two examples for which sledgehammer failed repeatedly.
what would be the simplest way to prove them?
lemma
fixes a::real
assumes "a>0"
shows "1/a - 1/(a+1) = 1/(a*(a+1))"
oops
lemma
fixes a b c :: real
assumes "a>0"
shows "((a powr c) + (b powr c)) powr 2 =
(a powr (2c)) + 2(a powr c)(b powr c) + (b powr (2c))"
oops
thnx, Noam
Email Gateway (Aug 22 2022 at 14:33):From: Makarius <makarius@sketis.net>
That is already quite old: the current release is Isabelle2016 (February
2016), and we are presently moving towards Isabelle2016-1 (December
2016) -- see also http://isabelle.in.tum.de/website-Isabelle2016-1-RC1
Makarius
Email Gateway (Aug 22 2022 at 14:33):From: Makarius <makarius@sketis.net>
That is already quite old: the current release is Isabelle2016 (February
2016), and we are presently moving towards Isabelle2016-1 (December
2016) -- see also http://isabelle.in.tum.de/website-Isabelle2016-1-RC1
Makarius
Email Gateway (Aug 22 2022 at 14:33):From: noam neer <noamneer@gmail.com>
well, the computer itself is much older.
does Isabelle 2016 require significantly more memory?
Email Gateway (Aug 22 2022 at 14:33):From: noam neer <noamneer@gmail.com>
well, the computer itself is much older.
does Isabelle 2016 require significantly more memory?
Email Gateway (Aug 22 2022 at 14:34):From: Makarius <makarius@sketis.net>
Not much. You should try.
A very old computer might be actually a source of these problems. The
minimal system requirements for Isabelle are 2 cores + 4 GB RAM. This is
not spelt out anywhere, because that is really minimal -- consumer
hardware from many years ago had this already.
Makarius
Email Gateway (Aug 22 2022 at 14:34):From: noam neer <noamneer@gmail.com>
I have an i3 processor and 4GB RAM.
but, does sledgehammer give the external provers a time limit,
a limit on the search space/number of deductions or no limit at all?
in the first case, I guess one can expect different computers will differ
not only in running time but in the actual results too.
Email Gateway (Aug 22 2022 at 14:34):From: Makarius <makarius@sketis.net>
Yes, there are many such policies built into it.
Apart from that, Windows can sometimes cause problems, e.g. via
Antivirus tools.
You should definitely try a newer Isabelle version: all aspects of the
system are monotonically improved. There is no point to try isolating
problems in old versions.
Makarius
Email Gateway (Aug 22 2022 at 14:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Sledgehammer is a very complicated subsystem of Isabelle, which attempts to prove subgoals using external provers. It is often successful, but of course, many problems are too difficult for it.
Your first problem looks like it would be quite easy if you call the simplifier using divide_simps (and don’t forget to include your assumption a>0).
And yes, you definitely need to use a recent version of Isabelle. I suggest that you download the release candidate,
http://isabelle.in.tum.de/website-Isabelle2016-1-RC2 <http://isabelle.in.tum.de/website-Isabelle2016-1-RC2>.
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC