# Re: [isabelle] Proving with Indexed Sums

Thank you Manuel and Johannes,

These explanations were very helpful and enlightening at the same time.

Best!

On Tue, Dec 11, 2012 at 11:28 AM, Manuel Eberl <eberlm at in.tum.de> wrote:

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

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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