Re: [isabelle] Proving with Indexed Sums



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. 2*j)" 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


On 11/12/12 13:49, Alfio Martini wrote:
> 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
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.