[isabelle] Difficulties with "setsum" · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Difficulties with "setsum"

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

From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,

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 ano 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.

My thy file is attached and, in the proof, is the only line with "sorry".
I would very grateful if anyone could take a quick look at that.

To get a better feeling of what are the underlying simplification rules,
I performed some tests with setsum, but the results were disappointing.
(see below).

Besides, acoording to "What is is Main", setsum is defined in "Finite_Set",
but in Isabelle 2014 it is defined in "Groups_Big".

(* Testing the setsum function *)
fun i2n::"int ⇒ nat" where
"i2n x = (if x ≤ 0 then 0 else Suc (i2n (x - 1)))"

value "int (setsum id {1::nat..5})" (* this works *)
lemma "setsum id {1::nat..2} = (Suc (Suc (Suc 0)))"
apply (auto) oops
lemma "setsum id {1::nat..5}= i2n 15"
apply (auto) oops
lemma "(setsum id {1::nat..2})= Suc (Suc (Suc 0))"
apply (auto) oops
lemma "(∑ k::nat ∈ {j. 1≤j ∧ j≤3}. k) = 6"
apply oops
lemma "(∑ k::nat | k≥1 ∧ k≤2 . k) = Suc (Suc (Suc 0))"
apply (auto) oops
lemma "(∑ k::nat=1..3. k)= (∑ k=1..2. k) + 3" oops
term "∑ k=1..n. k"
value "∑ k::nat = 2 ..1. k" (* this works *)
(* end of test *)

All the Best!
SumInt.thy

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

From: Alfio Martini <alfio.martini@acm.org>
Sorry, there was a typo in the previous theory file. It is attached again.

Best!
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Wed, Apr 22, 2015 at 11:46 AM
Subject: Difficulties with "setsum"
To: "cl-isabelle-users@lists.cam.ac.uk" <cl-isabelle-users@lists.cam.ac.uk>

Dear Isabelle Users,

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 ano 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.

My thy file is attached and, in the proof, is the only line with "sorry".
I would very grateful if anyone could take a quick look at that.

To get a better feeling of what are the underlying simplification rules,
I performed some tests with setsum, but the results were disappointing.
(see below).

Besides, acoording to "What is is Main", setsum is defined in "Finite_Set",
but in Isabelle 2014 it is defined in "Groups_Big".

(* Testing the setsum function *)
fun i2n::"int ⇒ nat" where
"i2n x = (if x ≤ 0 then 0 else Suc (i2n (x - 1)))"

All the Best!

--
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:21):

From: Manuel Eberl <eberlm@in.tum.de>
The problem is that in order to "unroll" the setsum, you first have to
bring the numerals (e.g. 2, 3, 4) into successor notation. One way to do
this is to add eval_nat_numeral to your simpset, e.g.

apply (auto simp: eval_nat_numeral)

Most of your example work automatically with these, but you will have to
massage expressions like "(∑ k::nat ∈ {j. 1≤j ∧ j≤3}. k)" by hand a bit
first, e.g. by proving that "{j. 1≤j ∧ j≤3} = {1..3}".

One could easily write simplification rules that unroll setsums over
constant intervals like these automatically or even write a simproc that
does that, but I don't think that would be very helpful in practice.

Cheers,

Manuel

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

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

Thanks for the feedback. But in my proof, I am working with integers and
that line
with "sorry" does not get proved with this lemma. The line with "sorry"
addresses the very definition
of indexed sums, I think.

Best!

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

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

I think that the main problem is that the automatic methods cannot cope
with following trivial
lemmas, although both sides evaluate correctly with the command 'value',

value "(setsum id {1::int..2}) + (3::int)"
value "(setsum id {1::int..3})"
lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3" oops
value "(setsum id {-3::int..3})"
value "(setsum id {-3::int..2}) + 3"
lemma "(setsum id {-3::int..3}) = (setsum id {-3..2}) + 3" oops

I tried sledgehammer but it does not find anything. Anyway, the last time
sledgehammer worked
fine for me was with Isabelle 2012.

Best!

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

From: Wenda Li <wl302@cam.ac.uk>
Hi Alfio,

Your sorry can be proved by:

also have "... = (∑ k=l..i+1. k)"
proof -
have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto
thus ?thesis by simp
qed

Also note, goals like this:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

if both sides can be evaluated to the same value, you can discharge the
goal by "eval".

Cheers,
Wenda

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

From: Alfio Martini <alfio.martini@acm.org>
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Wed, Apr 22, 2015 at 2:17 PM
Subject: Re: [isabelle] Difficulties with "setsum"
To: Wenda Li <wl302@cam.ac.uk>

Hi Wenda,

if both sides can be evaluated to the same value, you can discharge the
goal by "eval"

Great. Did not know this.

also have "... = (∑ k=l..i+1. k)"

proof -
have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto
thus ?thesis by simp
qed

Very clever. Thanks a lot!!

Best!

On Wed, Apr 22, 2015 at 2:07 PM, Wenda Li <wl302@cam.ac.uk> wrote:

Hi Alfio,

Your sorry can be proved by:

also have "... = (∑ k=l..i+1. k)"
proof -
have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto
thus ?thesis by simp
qed

Also note, goals like this:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

if both sides can be evaluated to the same value, you can discharge the
goal by "eval".

Cheers,
Wenda

On 2015-04-22 17:24, Alfio Martini wrote:

Hi,

I think that the main problem is that the automatic methods cannot cope
with following trivial
lemmas, although both sides evaluate correctly with the command 'value',

value "(setsum id {1::int..2}) + (3::int)"
value "(setsum id {1::int..3})"
lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3" oops
value "(setsum id {-3::int..3})"
value "(setsum id {-3::int..2}) + 3"
lemma "(setsum id {-3::int..3}) = (setsum id {-3..2}) + 3" oops

I tried sledgehammer but it does not find anything. Anyway, the last time
sledgehammer worked
fine for me was with Isabelle 2012.

Best!

On Wed, Apr 22, 2015 at 12:00 PM, Manuel Eberl <eberlm@in.tum.de> wrote:

The problem is that in order to "unroll" the setsum, you first have to

bring the numerals (e.g. 2, 3, 4) into successor notation. One way to do
this is to add eval_nat_numeral to your simpset, e.g.

apply (auto simp: eval_nat_numeral)

Most of your example work automatically with these, but you will have to
massage expressions like "(∑ k::nat ∈ {j. 1≤j ∧ j≤3}. k)" by hand a bit
first, e.g. by proving that "{j. 1≤j ∧ j≤3} = {1..3}".

One could easily write simplification rules that unroll setsums over
constant intervals like these automatically or even write a simproc that
does that, but I don't think that would be very helpful in practice.

Cheers,

Manuel

On 22/04/15 16:46, Alfio Martini wrote:

Dear Isabelle Users,

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 ano 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.

My thy file is attached and, in the proof, is the only line with
"sorry".
I would very grateful if anyone could take a quick look at that.

To get a better feeling of what are the underlying simplification rules,
I performed some tests with setsum, but the results were disappointing.
(see below).

Besides, acoording to "What is is Main", setsum is defined in
"Finite_Set",
but in Isabelle 2014 it is defined in "Groups_Big".

(* Testing the setsum function *)
fun i2n::"int ⇒ nat" where
"i2n x = (if x ≤ 0 then 0 else Suc (i2n (x - 1)))"

value "int (setsum id {1::nat..5})" (* this works *)
lemma "setsum id {1::nat..2} = (Suc (Suc (Suc 0)))"
apply (auto) oops
lemma "setsum id {1::nat..5}= i2n 15"
apply (auto) oops
lemma "(setsum id {1::nat..2})= Suc (Suc (Suc 0))"
apply (auto) oops
lemma "(∑ k::nat ∈ {j. 1≤j ∧ j≤3}. k) = 6"
apply oops
lemma "(∑ k::nat | k≥1 ∧ k≤2 . k) = Suc (Suc (Suc 0))"
apply (auto) oops
lemma "(∑ k::nat=1..3. k)= (∑ k=1..2. k) + 3" oops
term "∑ k=1..n. k"
value "∑ k::nat = 2 ..1. k" (* this works *)
(* end of test *)

All the Best!

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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

From: Lars Hupel <hupel@in.tum.de>
Note that 'eval' does not go through the kernel and is generally
considered bad style (except for maybe exploratory purposes).

Fortunately, there's an alternative:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"
by code_simp

This sets uses the same code equations as 'eval' (as far as I know), but
goes through the kernel (by invoking the simplifier).

Cheers
Lars

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

From: Tobias Nipkow <nipkow@in.tum.de>
On 22/04/2015 21:17, Lars Hupel wrote:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

if both sides can be evaluated to the same value, you can discharge the
goal by "eval".

Note that 'eval' does not go through the kernel and is generally
considered bad style (except for maybe exploratory purposes).

I disagree. I have seen too many people wasting their time trying to achieve
something by "pure inference" that eval will do without blinking an eye. There
is no evidence that the evaluator is less reliable than the inference kernel. Of
course in this example you may as well use code_simp, but the latter can be
prohibitively slow.

Tobias

Fortunately, there's an alternative:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"
by code_simp

This sets uses the same code equations as 'eval' (as far as I know), but
goes through the kernel (by invoking the simplifier).

Cheers
Lars

smime.p7s

Last updated: Nov 21 2024 at 12:39 UTC