[isabelle] Difficulties with "setsum" (Alfio Martini) · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Difficulties with "setsum" (Alfio Martini)

Email Gateway (Aug 22 2022 at 09:22):

From: "W. Douglas Maurer" <maurer@gwu.edu>
On 22 Apr 2015, Alfio Martini <alfio.martini@acm.org> wrote:

While trying to prove the correctness of a simple function that returns
the sum of the values between integers l and u, I stumbled upon
an unexpected problem: I was not able to prove that

(Sum k=l..(u+1). k) = (u+1) + (Sum k=l...u) if l<u+1, which should
hold by the definition of an indexed sum.

I asked this question on March 6th, 2015, in the following more general form:

I am having problems with forward proofs by induction. I would like
for Isar to be able to prove that 1+4+9+...+n*n =
(n(n+1)(2*n+1))/6 and the like. In order to do the inductive
proof, I have to know that m<=n implies (f(m)+f(m+1)+...+f(n+1)) =
(f(m)+f(m+1)+...+f(n))+f(n+1), for integers m and n. In Isar, this
becomes that m<=n implies (setsum f {m..n+1} = (setsum f {m..n}) +
f(n+1)). This would seem to be a fundamental rule, and yet I cannot
seem to find it anywhere in either the library or the supplemental
library.

This appeared in Cl-isabelle-users Digest, Vol 117, Issue 10, #6, and
Andreas Lochbihler replied to it as follows:

There are far fewer theorems about setsum over intervals of integers
than over natural numbers. Still, there are enough theorems in the
library to prove what you want. Sledgehammer finds the following
proof for me:

lemma "m ? n ? setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)"
by(metis add.commute atLeastAtMostPlus1_int_conv
atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
finite_atLeastAtMost_int linear not_less setsum.insert
zle_add1_eq_le)

Hope this helps,
Andreas

This appeared in Cl-isabelle-users Digest, Vol 117, Issue 10, #7.

Email Gateway (Aug 22 2022 at 09:22):

From: Alfio Martini <alfio.martini@acm.org>
Hi Douglas,

I followed that discussion very closely. In fact, from those messages
I took the idea of structuring the proof that I emailed in a previous
thy file in this thread. Somehow I have missed this particular remark
from Andreas who is, amongst many other experts in this list,
always very helpful.

There are far fewer theorems about setsum over intervals of integers than

Email Gateway (Aug 22 2022 at 09:22):

From: Makarius <makarius@sketis.net>
There is Isabelle2015-RC1 already, to try if the situation has improved.
If not, we also need a bit of information about your hardware and
operating system version.

I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.

Makarius

Email Gateway (Aug 22 2022 at 09:23):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,

There is Isabelle2015-RC1 already, to try if the situation has improved. If

not, we also need a bit of information about your hardware and operating
system version.
I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.

My machine (laptop) configuration:

Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor

Lemmas I tried with sledgehammer

lemma "[a] = [b] ⟹ a = b" oops
lemma aux: "m < n+1 ⟹setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
oops

When I run the theory file (attached) with Isabelle2015-RC1 I get the
following messages in the output window:

Sledgehammering...

"remote_vampire": Error: SystemOnTPTP is not available.

"spass": Timed out.
"cvc4": Timed out.
"z3": Timed out

And with Isabelle2014, similar messages appear:

"remote_vampire": Error: SystemOnTPTP is not available.

"z3": Timed out.
"e": Timed out.
"spass": Timed out.

One information might be useful: Usually (but not always) I have to exit
Chrome before starting
Isabelle 2014 or Isabelle 2015-RC1. Otherwise I get the error message:
"error starting Java VM".

Thank you in advance for any help with this. I never complained before
about this because I always felt guilty when using sledgehammer. I had the
impression
that I did not wanted to work hard enough. That I was cheating.
But that feeling of guilt does not exists anymore. Hopefully it is not
because
I gave up working hard.

Best!

On Thu, Apr 23, 2015 at 6:28 AM, Makarius <makarius@sketis.net> wrote:

On Wed, 22 Apr 2015, Alfio Martini wrote:

I use the Windows installation of Isabelle 2014 and my sledgehammer

installation does not find any proof for this lemma. Actually, it never
finds any proof whatsoever. I have just realized that it does not solve
even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
have always used Sledgehammer as it is packaged. I just set z3
non-commercial
use to "yes". The prover "remote-vampire" is never available (literally),
while e, spass and z3 always time out.

I will have to take a look into this. This is really making may Isabelle
experience miserable at the moment.

There is Isabelle2015-RC1 already, to try if the situation has improved.
If not, we also need a bit of information about your hardware and operating
system version.

I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.

Makarius

Email Gateway (Aug 22 2022 at 09:23):

From: Alfio Martini <alfio.martini@acm.org>
Forgot to attatch the theory file.
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Thu, Apr 23, 2015 at 4:01 PM
Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
To: Makarius <makarius@sketis.net>, "cl-isabelle-users@lists.cam.ac.uk" <
cl-isabelle-users@lists.cam.ac.uk>

Hi Makarius,

There is Isabelle2015-RC1 already, to try if the situation has improved. If

not, we also need a bit of information about your hardware and operating
system version.
I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.

My machine (laptop) configuration:

Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor

Lemmas I tried with sledgehammer

lemma "[a] = [b] ⟹ a = b" oops
lemma aux: "m < n+1 ⟹setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
oops

When I run the theory file (attached) with Isabelle2015-RC1 I get the
following messages in the output window:

Sledgehammering...

"remote_vampire": Error: SystemOnTPTP is not available.

"spass": Timed out.
"cvc4": Timed out.
"z3": Timed out

And with Isabelle2014, similar messages appear:

"remote_vampire": Error: SystemOnTPTP is not available.

"z3": Timed out.
"e": Timed out.
"spass": Timed out.

One information might be useful: Usually (but not always) I have to exit
Chrome before starting
Isabelle 2014 or Isabelle 2015-RC1. Otherwise I get the error message:
"error starting Java VM".

Best!

On Thu, Apr 23, 2015 at 6:28 AM, Makarius <makarius@sketis.net> wrote:

On Wed, 22 Apr 2015, Alfio Martini wrote:

I use the Windows installation of Isabelle 2014 and my sledgehammer

installation does not find any proof for this lemma. Actually, it never
finds any proof whatsoever. I have just realized that it does not solve
even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
have always used Sledgehammer as it is packaged. I just set z3
non-commercial
use to "yes". The prover "remote-vampire" is never available (literally),
while e, spass and z3 always time out.

I will have to take a look into this. This is really making may Isabelle
experience miserable at the moment.

There is Isabelle2015-RC1 already, to try if the situation has improved.
If not, we also need a bit of information about your hardware and operating
system version.

I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.

Makarius

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Email Gateway (Aug 22 2022 at 09:25):

From: Makarius <makarius@sketis.net>
On Thu, 23 Apr 2015, Alfio Martini wrote:

My machine (laptop) configuration:

Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor

Fine so far. It is an up-to-date low-end machine and should work without
problems, at least in theory.

Lemmas I tried with sledgehammer

lemma "[a] = [b] ⟹ a = b" oops
lemma aux: "m < n+1 ⟹setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
oops

When I run the theory file (attached) with Isabelle2015-RC1 I get the
following messages in the output window:

Sledgehammering...

"remote_vampire": Error: SystemOnTPTP is not available.

"spass": Timed out.
"cvc4": Timed out.
"z3": Timed out

I've tried this with Isabelle2015-RC2. It is generally better to test
sledgehammer with these parameters:

sledgehammer_params [dont_try0]

Doing that, it basically works for me (on 12 cores), but cvc4 breaks down
as follows:

SMT: Result:
(error "Error in option parsing: option `produce-unsat-cores' requires a proofs-enabled build of CVC4; this binary was not built with proof support")
"cvc4": A prover error occurred:
Solver "cvc4" failed -- enable tracing using the "smt_trace" option for details

This means there is something wrong with the bundled cvc4 component, and
Jasmin needs to look at it.

Makarius

Email Gateway (Aug 22 2022 at 09:25):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius and Jasmim,

Even with dont_try0 as a sledgehammer parameter, I get the same old timeout
results both
with Isa2014 and Isa2015-RC1. I haven´t tried with Isa2015RC2 yet,

Best!.

Email Gateway (Aug 22 2022 at 09:25):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Makarius,

It turns out the Windows binary is compiled without proof output. CVC4’s predecessor, CVC3, used to only work in that mode, but CVC4 now supports unsat core output (i.e. it can print the list of used axioms for a proof, which is useful to Sledgehammer). Unfortunately, the CVC4 developers compile out proof output from CVC4.

The ultimate solution will be to build a proper binary for CVC4 for Windows, but I’m currently not in a position to do it. (I need to get a Windows license first etc., and I’m not at the lab next week.)

What I have to offer instead is less efficient: brute-force minimization. This is what we used to do with CVC3 and Yices. It works surprisingly well, esp. that CVC4 is blindingly fast. Please apply the following exported patch to “isabelle-release”.

Thanks,

Jasmin
cvc4.export

Email Gateway (Aug 22 2022 at 09:25):

From: Makarius <makarius@sketis.net>
That CPU has 2 cores and hyperthreading, i.e. 4 virtual cores. Can you
try this:

ML "Multithreading.max_threads_value ()"

There is some chance that it gives 4, because Cygwin is not reliable in
reporting virtual CPU cores. Since starting external processes in
parallel imposes an extra load on Cygwin, it might explain the timeout of
the provers.

The Isabelle/jEdit plugin options offer the possibility to set "threads"
explicitly, e.g. to 2. Does this change the situation?

Makarius

Email Gateway (Aug 22 2022 at 09:26):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,

At least I got some progress, yet the overall situation is still far from
ideal.

I got the best results with Threads=1 (instead of the default 0). "ML
Multithreading..." returns 4.
Following your suggestions, here is the summary of my tests with 2014, RC1
and RC2.

It seems that 2014 is the best option so far. So what is next?

Best!

Isabelle 2014
sledgehammer_params [dont_try0] (* can't be used, otherwise
sledgehammer runs forever and can't be canceled. I had to kill
Isabelle *)

Num. Threads = 1

lemma "[a] = [b] ==> a = b"
"e": Try this: by (metis the_elem_set) (13 ms).
"spass": Timed out.
"remote_vampire": Try this: by (metis list.inject) (15 ms).
"z3": Try this: by (metis list.inject) (19 ms).

lemma aux: "m < n+1 ==> setsum f {m..n + 1} =
setsum f {m..n} + f (n + 1 :: int)"
"e": Timed out.
"spass": Timed out.
"remote_vampire": Timed out.
"z3": Timed out.

Isabelle RC1
sledgehammer_params [dont_try0] (* mandatory *)
Num. Threads = 1

lemma "[a] = [b] ==> a = b"

"cvc4": Timed out.
"remote_vampire": Try this: by (metis list.inject) (63 ms).
"z3": Try this: by (metis list.inject) (63 ms).
"spass": Try this: by (metis list.inject) (31 ms).
"e": Try this: by (metis the_elem_set) (62 ms).

Isabelle RC2
sledgehammer_params [dont_try0] (* mandatory *)
Num_Threads = 1

lemma "[a] = [b] ==> a = b"

"cvc4": A prover error occurred:
Solver "cvc4" failed -- enable tracing using the "smt_trace" option for
details
"remote_vampire": Try this: by (metis list.inject) (63 ms).
"z3": Try this: by (metis list.inject) (47 ms).
"spass": Timed out.
"e": Try this: by (metis append_Cons append_Nil list.inject) (62 ms).

Email Gateway (Aug 22 2022 at 09:26):

From: Makarius <makarius@sketis.net>
Next you can try the adhoc snapshot
http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
contains the change of CVC4 by Jasmin, and a checkbox to control the
"try0" or "dont_try0" option in the Sledgehammer panel.

Your SledgeFail.thy contains two examples:

lemma "[a] = [b] ⟹ a = b"

lemma "m < n + 1 ⟹ setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)"

The first works smoothly for me with or without "try methods", both on
Linux and Windows.

The second takes a bit longer to produce the following results (without
"try methods"). The following is on Linux:

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (122 ms).
"e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
finite_atLeastAtMost_int less_irrefl setsum.insert zle_add1_eq_le zless_add1_eq) (761 ms).
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (158 ms).
"spass": Timed out.
"remote_vampire": Timed out.

This is on Windows 7, with sledgehammer_timeout = 60 (see plugin options):

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (203 ms).
"remote_vampire": Timed out.
"spass": Timed out.
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (1.2 s).
"e": Timed out.

That is less than nothing, although not as smooth as on a proper Unix
system.

Do you have an extra virus checker that somehow delays external program
execution?

Makarius

Email Gateway (Aug 22 2022 at 09:26):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,

First of all, many thanks for helping me working around this problem, and
during the weekend!

Do you have an extra virus checker that somehow delays external program
execution?
Good point. I have found some obscure McAffe internet security software in
my machine. I do not
know how it got there. I only use Avast. Anyway, I deleted and used time
out = 60.

Now I solve the harder lemma both in Isabelle 2014 and Isabelle 2015-RC2. I
will
remove cvc4 from the provers list until that bug is corrected. Things get
much faster
without it. In any case, sledgehammer seems to solve problems a lot faster
in Isabelle
2014 than in RC2. Who would expect that?

Here are my results. Thanks a lot!

Isabelle 2014
sledgehammer_params [dont_try0] (* can't be used, otherwise
sledgehammer runs forever and can't be canceled. I had to kill
Isabelle *)

Num. Threads = 1

lemma aux: "m < n+1 ==> setsum f {m..n + 1} =
setsum f {m..n} + f (n + 1 :: int)"
"e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int linorder_not_less set_upto
setsum.insert zle_add1_eq_le zless_add1_eq) (1.15 s).
"spass": Timed out.
"remote_vampire": Timed out.
"z3": Timed out.

Isabelle RC2
sledgehammer_params [dont_try0] (* mandatory *)
timeout = 60
Num_Threads = 1

lemma aux: "m < n+1 ==> setsum f {m..n + 1} =
setsum f {m..n} + f (n + 1 :: int)"
"cvc4": A prover error occurred:
Solver "cvc4" failed -- enable tracing using the "smt_trace" option for
details
"remote_vampire": Timed out.
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_upto atLeastLessThanPlusOne_atLeastAtMost_int
atLeastLessThan_iff finite_atLeastAtMost_int setsum.insert) (> 1.0 s, timed
out).
"spass": Timed out.
"e": Timed out.

Email Gateway (Aug 22 2022 at 09:28):

From: Makarius <makarius@sketis.net>
This is bounced back to isabelle-users. I am actually not the expert on
sledgehammer, only the (sole?) maintainer of multiplatform support.

Makarius

---------- Forwarded message ----------
Date: Mon, 27 Apr 2015 17:28:24 -0300
From: Alfio Martini <alfio.martini@acm.org>
To: Makarius <makarius@sketis.net>
Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

HI Makarius,

Next you can try the adhoc snapshot

http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
contains the change of CVC4 by Jasmin, and a checkbox to control the "try0"
or "dont_try0" option in the Sledgehammer panel.

I have tried this snapshot version and it fails to solve that lemma about
indexed sums. All provers time out with sledgehammer_params [dont_try0,
timeout=60] .

I set up Avast not consider any Isabelle directory, but I am sure that it
is not the problem. Meanwhile,
I installed a virtual machine with Linux Mint and installed Isabelle 2014.
Sledgehammer works
reasonably well with Threads = 1, without try methods and with timeout=60,
especially with
Z3, which seems to be the best of them by far. I will wait for
RC3 and test again with Windows & Linux. In the worst case scenario, I will
use Isabelle normally
on Windows and if I need sledgehammer, then I will use it in my virtual
Linux installation. My God,
the look and feel of Isabelle/jEdit in Linux it is not that pretty (to put
it mildly), especially if one is already used
to the Windows version.

I am not sending these messages to the list anymore. It is just me that is
having this problem,
I think.

Best!

On Sat, Apr 25, 2015 at 5:48 PM, Makarius <makarius@sketis.net> wrote:

On Sat, 25 Apr 2015, Alfio Martini wrote:

At least I got some progress, yet the overall situation is still far from

ideal.

I got the best results with Threads=1 (instead of the default 0). "ML
Multithreading..." returns 4. Following your suggestions, here is the
summary of my tests with 2014, RC1 and RC2.

It seems that 2014 is the best option so far. So what is next?

Next you can try the adhoc snapshot
http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
contains the change of CVC4 by Jasmin, and a checkbox to control the "try0"
or "dont_try0" option in the Sledgehammer panel.

Your SledgeFail.thy contains two examples:

lemma "[a] = [b] ⟹ a = b"

lemma "m < n + 1 ⟹ setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"

The first works smoothly for me with or without "try methods", both on
Linux and Windows.

The second takes a bit longer to produce the following results (without
"try methods"). The following is on Linux:

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (122 ms).
"e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv
atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
finite_atLeastAtMost_int less_irrefl setsum.insert zle_add1_eq_le
zless_add1_eq) (761 ms).
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (158 ms).
"spass": Timed out.
"remote_vampire": Timed out.

This is on Windows 7, with sledgehammer_timeout = 60 (see plugin options):

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (203 ms).
"remote_vampire": Timed out.
"spass": Timed out.
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (1.2 s).
"e": Timed out.

That is less than nothing, although not as smooth as on a proper Unix
system.

Do you have an extra virus checker that somehow delays external program
execution?

Makarius

Email Gateway (Aug 22 2022 at 09:28):

From: Makarius <makarius@sketis.net>
On Mon, 27 Apr 2015, Makarius wrote:

---------- Forwarded message ----------
Date: Mon, 27 Apr 2015 17:28:24 -0300
From: Alfio Martini <alfio.martini@acm.org>
To: Makarius <makarius@sketis.net>
Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

I installed a virtual machine with Linux Mint and installed Isabelle 2014.

Linux Mint had a lot of attention initially, but was of rather bad quality
the last time I checked it (which is already 1-2 years ago). For me the
canonical Linux distribution remains Ubuntu (or Xubuntu) despite the may
attempts to ruin the open-source OS world by endless forks.

My God, the look and feel of Isabelle/jEdit in Linux it is not that
pretty (to put it mildly), especially if one is already used to the
Windows version.

That is normal on Linux/X11.
On Windows and Mac OS X, the rendering is
fine. I usually use Mac OS X for presentation, and restrict Linux to
private use at home, when nobody is looking.

Makarius

Email Gateway (Aug 22 2022 at 09:29):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
On 28 April 2015 07:18:47 GMT+10:00, Makarius <makarius@sketis.net> wrote:

On Mon, 27 Apr 2015, Makarius wrote:

---------- Forwarded message ----------
Date: Mon, 27 Apr 2015 17:28:24 -0300
From: Alfio Martini <alfio.martini@acm.org>
To: Makarius <makarius@sketis.net>
Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

I installed a virtual machine with Linux Mint and installed Isabelle
2014.

Linux Mint had a lot of attention initially, but was of rather bad
quality
the last time I checked it (which is already 1-2 years ago). For me
the
canonical Linux distribution remains Ubuntu (or Xubuntu) despite the
may
attempts to ruin the open-source OS world by endless forks.

FWIW one of my machines has run Isabelle on Linux Mint for the last 2 years with no problems. My own experience is that Mint is now more stable and polished than Xubuntu, though Ubuntu still gets the most UI/UX attention, and these things are obviously subjective.

My God, the look and feel of Isabelle/jEdit in Linux it is not that
pretty (to put it mildly), especially if one is already used to the
Windows version.

That is normal on Linux/X11.
On Windows and Mac OS X, the rendering is

fine. I usually use Mac OS X for presentation, and restrict Linux to
private use at home, when nobody is looking.

This is not really an Isabelle/jEdit issue, but rather that Java (or Java developers?) makes only a token effort at making its applications look/behave like native applications.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Email Gateway (Aug 22 2022 at 09:29):

From: Makarius <makarius@sketis.net>
The problem here is that there is no native UI framework on Linux. Or do
you mean Motif? It is still supported by Java/AWT/Swing, but unusable.

GTk is sometimes considered native, but it is merely one of many forks
that make the platform a big mess. I do use the GTk look-and-feel of
Java/Swing myself, because it does the GUI scaling almost right -- this is
essential for 4K displays.

Makarius

Email Gateway (Aug 22 2022 at 09:29):

From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
I did not mean any specific framework, as I'm not even familiar with the latest Java UI options. I
meant that when you open a Java application, it is immediately obvious to you from the UI and
behaviour that it is a Java application.

You're right that I potentially muddied the waters by using "native" to mean GTK. I consider GTK
"native" on Gnome (+ Cinnamon, etc.). To clarify my comments, I wasn't meaning this as a criticism
of the Java platform. Applications from other ecosystems like KDE and Wine look equally out of place
in a GTK environment.

Email Gateway (Aug 22 2022 at 09:29):

From: "W. Douglas Maurer" <maurer@gwu.edu>
I've been following the 'Difficulties with "setsum"' thread for some
time now, and, after much discussion, I still don't know what the
best way is, to introduce the lemma 'aux:' above into my proofs. I
need it in order, for example, to prove:
"1^2-2^2+3^2-4^2+...+(-1)^(n+1)*n^2 = ((-1)^(n+1))n(n+1)/2"
This one has to be done by using int, not nat, because the answer
might be negative. There are over a dozen others, given as exercises
on pp. 49-50 of Johnsonbaugh, R., "Discrete Mathematics" (2nd
edition). My ultimate goal (which will probably take over a year to
get off the ground) is for students of discrete mathematics to get
started with at least the lowest-level features of Isar as part of
their study. I can get them through proofs by contradiction, proofs
by cases, and (if they involve exponents, such as proving that 8^k -
2^k is always divisible by 6), proofs by induction, since exponents
are natural numbers; but I'm stuck, on more general proofs by
induction, until I can somehow introduce this one fact (aux: above).
-WDMaurer

Email Gateway (Aug 22 2022 at 09:29):

From: Tobias Nipkow <nipkow@in.tum.de>
On 28/04/2015 06:58, W. Douglas Maurer wrote:

Lemmas I tried with sledgehammer

lemma "[a] = [b] ? a = b" oops
lemma aux: "m < n+1 ?setsum f {m..n+1} = setsum f {m..n} + f (n+1 :: int)"

I asked sledgehammer and it told me

by (simp add: add.commute atLeastAtMostPlus1_int_conv)

Maybe my s/h is bigger (or more recent) than yours ;-)

Tobias

oops

I've been following the 'Difficulties with "setsum"' thread for some time now,
and, after much discussion, I still don't know what the best way is, to
introduce the lemma 'aux:' above into my proofs. I need it in order, for
example, to prove:
"1^2-2^2+3^2-4^2+...+(-1)^(n+1)*n^2 = ((-1)^(n+1))n(n+1)/2"
This one has to be done by using int, not nat, because the answer might be
negative. There are over a dozen others, given as exercises on pp. 49-50 of
Johnsonbaugh, R., "Discrete Mathematics" (2nd edition). My ultimate goal (which
will probably take over a year to get off the ground) is for students of
discrete mathematics to get started with at least the lowest-level features of
Isar as part of their study. I can get them through proofs by contradiction,
proofs by cases, and (if they involve exponents, such as proving that 8^k - 2^k
is always divisible by 6), proofs by induction, since exponents are natural
numbers; but I'm stuck, on more general proofs by induction, until I can somehow
introduce this one fact (aux: above). -WDMaurer
smime.p7s

Email Gateway (Aug 22 2022 at 09:53):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Alfio,

It is hard to make any definite judgment on the basis of a single example. This is even more true because Sledgehammer, since Isabelle2014, uses machine learning. This means that if you try to prove a goal that is similar (or identical) to a formula you have already proved, it is likely to be faster the second time around. Machine learning must be disabled before taking any measurements.

In the past months, in fact, also weeks, we have run evaluations of Sledgehammer, and the results look as usual. In fact, 2015-RC should be a bit better than 2014, thanks to improvements both to the machine learning (MaSh) and the Isar proof generation framework, including the new one-liner proofs with various proof methods (“simp”, “auto”, “blast”, etc.).

However, there has been some bugs in that last feature (witness Lars Hupel’s bug report, which I answered tonight), and there might be technical issues on Windows. If you have the clear impression that Sledgehammer is weaker and can repeat this on many examples, ideally with the “fact_filter = mepo” option (using the “sledgehammer” command directly, or “sledgehammer_params”), I would like to hear again from you.

Sledgehammer should be becoming better, not worse.

As for CVC4, we will look into building a Windows executable for it with proof output enabled, which should make it fast — in fact, the best prover by a good margin.

Cheers,

Jasmin

Last updated: Nov 21 2024 at 12:39 UTC