Email Gateway (Aug 19 2022 at 09:29): Email Gateway (Aug 19 2022 at 09:29):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I wonder if there is a better way to express the summations below in
Isabelle/HOL/Isar (I might think
there is).
In particular, I do not get why the first two theorems express the subgoals
in term of the "lowest" level
terms "setsum" and "op" while the third one thankfully not. Especially, I
don´t see any "relevant" difference
between sum_patter02 e sum_pattern03.
As a last unrelated question, in theorem sum_pattern04, I could not prove
the inductive step with either
simp or auto. When using exponentiations, what kind of proof method does
one has to usually use?
Thanks for any help!
theorem sum_pattern01:
fixes n::nat
shows "(∑j∈{0..n}. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qed
theorem sum_pattern02:
fixes n::nat
shows "(∑j=0..n. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qed
theorem sum_pattern03:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1) * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp
qed
theorem sum_pattern04:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1)^2" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp (* fails *)
qed
Email Gateway (Aug 19 2022 at 09:29):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Dienstag, den 11.12.2012, 10:49 -0200 schrieb Alfio Martini:
Dear Isabelle Users,
I wonder if there is a better way to express the summations below in
Isabelle/HOL/Isar (I might think there is).
I assume you want to try different ways to write down your lemma. If you
just need Gauss summation there are a couple of lemmas in Set_Interval
(gauss_sum and arith_sums_general), just use
find_theorems setsum "_ * _" .
In particular, I do not get why the first two theorems express the subgoals
in term of the "lowest" level
terms "setsum" and "op" while the third one thankfully not.
First "∑j=0..n. 2j" is just a different syntax for "∑j∈{0..n}. 2j" the
proof methods in Isabelle do not see any difference. So sum_pattern01
and sum_pattern02 are exactly the same theorems.
What is the difference between sum_pattern02 and sum_pattern03:
Isabelle applies eta normalization before it stores/displays terms
"%x. f x" is rewritten to f
so "SUM j : A. 2 * j"
-display->
"setsum A (%j. 2 * j)"
-eta->
"setsum A (op * 2)"
there is no syntax defined for the last term so it is displayed as is.
For sum_pattern03 eta normalization does not change the term.
Especially, I
don´t see any "relevant" difference
between sum_patter02 e sum_pattern03.
%j. 2 * j -eta-> op * 2
whereas
%j. 2 * j + 1 is not eta reducible.
As a last unrelated question, in theorem sum_pattern04, I could not prove
the inductive step with either
simp or auto. When using exponentiations, what kind of proof method does
one has to usually use?
Isabelle does not automatically unfold "t^2" as t might be a quite big
term. Use simp add: power2_eq_square to solve this.
Thanks for any help!
theorem sum_pattern01:
fixes n::nat
shows "(∑j∈{0..n}. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qedtheorem sum_pattern02:
fixes n::nat
shows "(∑j=0..n. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qedtheorem sum_pattern03:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1) * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp
qedtheorem sum_pattern04:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1)^2" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp (* fails *)
qed
Email Gateway (Aug 19 2022 at 09:29):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
This is the normal way of writing sums in Isabelle.
I think the reason for the behaviour of the output is that in case of
the first two lemmas, you have the statement "setsum (λj. 2*j) {0..n}".
"∑j=0..n. 2*j" is merely an abbreviation for that.
However, the term "(λj. 2j)" is morally "(λj. (op) 2 j)", which
η-reduces automatically to "(op* 2)", and my guess is that the pretty
printer cannot match this to the abbreviation for setsum anymore, so
that you get the "naked" output "setsum (op * 2) {0..n}".
In the other two lemmas, you have "setsum (λj. 2*j + 1) {0..n}". This
does not η- or β-reduce to anything, so Isabelle can show it in its
abbreviated form in the output.
A quick workaround for the first two lemmas would be two write them in a
form in which they are not η-reducible anymore, e.g. with "(λj. j*2)",
which is morally "(λj. (op*) j 2)". If you write your sum as "∑j∈{0..n}.
j*2", you get the nice output without setsum.
Regarding your last question, simp does the trick, but it needs the
lemma power2_eq_square, which states that "?a² = ?a * ?a". If you use
"simp add: power2_eq_square", your proof goes through automatically.
Normally, sledgehammer is a very good tool to find theorems like that,
but in this case, it doesn't work for some reason. In any case, if you
are in a situation like that, it can often help to do "apply simp" or
"apply auto" and examine where they get stuck. In this case, you can see
that the problem is that they cannot simplify the squared terms any
further, which is because simp doesn't "know" what squaring means.
Therefore, you need power2_eq_square to allow it to simplify the terms
further.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 09:29):From: Alfio Martini <alfio.martini@acm.org>
Thank you Manuel and Johannes,
These explanations were very helpful and enlightening at the same time.
Best!
Last updated: Nov 21 2024 at 12:39 UTC