Alexandre Soares (Sep 24 2024 at 18:27): Alexandre Soares (Sep 24 2024 at 18:27):I wrote the proof below, where I chain a lot of equations whose left-hand side are all equal. Is there any way to avoid keeping repeating the left-hand side?
lemma "sumsq n = n * (n + 1) * (2*n + 1) div 6"
proof (induction n)
case 0
show ?case by (simp)
next
case (Suc n)
fix n::nat
assume ih: "sumsq n = n * (n + 1) * (2 * n + 1) div 6"
have "sumsq (Suc n) = sumsq n + (Suc n)^2" by simp
then have "sumsq (Suc n) = n * (n + 1) * (2 * n + 1) div 6 + (Suc n)^2" by (simp add: ih)
then have "sumsq (Suc n) = n * (n + 1) * (2 * n + 1) div 6 + (n + 1)^2" by auto
then have "sumsq (Suc n) = n * (n + 1) * (2 * n + 1) div 6 + (n^2 + 2*n + 1)" using l1 by auto
then have "sumsq (Suc n) = (n * (n + 1) * (2 * n + 1) + 6 *(n^2 + 2*n +1)) div 6" by auto
then have "sumsq (Suc n) = (n + 1) * (n + 2) * (2 * n + 3) div 6" by (metis l3)
then show "sumsq (Suc n) = Suc n * (Suc n + 1) * (2 * Suc n + 1) div 6" by (metis l4)
qed
have "A=B" / also have "... =C" /also have "... = D" /finally (*A=D is the conclusion of the chain*)
Alexandre Soares (Sep 24 2024 at 19:34):@Mathias Fleury excellent, thanks!
Alexandre Soares (Sep 24 2024 at 23:43):@Mathias Fleury I just found this exact answer is on p. 47 of "Programming and Proving". If only I kept reading instead of rushing to ask... :speechless: Sorry!
Last updated: Dec 21 2024 at 16:20 UTC