proof of correctness for summation function with a counter

Question

Given the following summation function:

function sum :: "nat ⇒ nat ⇒ nat" where
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"
by pat_completeness auto
termination sum
apply (relation "measure (λ(i,N). N + 1 - i)")
apply auto
done

The stop condition is based on the N and i. I normally perform the induction on lists so I do not really know how to prove this function.

Can you please provide a solution and explanation of the next proof?

lemma sum_general[simp] : "c ≤ n ⟹ 2 * sum c n + (c - 1) * c = n * (n + 1)

You should first clarify what you mean by ‘correctness theorem’ here. Do you want to relate the function you defined to the standard summation operator in Isabelle-HOL? Do you want to prove a closed form for this sum? Also note that while you can do it this way, it is usually nicer to do the recursion downwards rather than upwards as you did. — Manuel Eberl
@ManuelEberl I come from Coq background, and this function really looked very interesting to me. I did a quick search, and I found this definition on page 4 of isabelle.in.tum.de/doc/functions.pdf. I come with a general lemma, lemma sum_general[simp] : "c ≤ n ⟹ 2 * sum c n + (c - 1) * c = n * (n + 1)", but I can't apply well_founded induction on c <= n. Any hint would be great. — keep_learning
@keep_learning I will add the lemma to my main question thanks. — P. Ez

Manuel Eberl Manuel Eberl · Accepted Answer · 2019-05-14T13:55:02

When you want to prove something about a recursively-defined function that you defined by the function command and where the recursion goes beyond primitive recursion, the best way is typically to use the induction rule that the function command gives you:

lemma "i ≤ N ⟹ N * Suc N = 2 * sum i N + i * (i - 1)"
proof (induction i N rule: sum.induct)
  case (1 i N)
  show ?case
  proof (cases "i = N")
  case True
  thus ?thesis sorry
next
  case False
  thus ?thesis sorry
qed

This gives you access to the induction hypothesis as "1.IH". I also already added the case distinction that you're going to need.

Note that the function package registers the defining equation of sum (sum.simps) as a simp rule. This is not a great idea here because it can make the simplifier loop since the equation is not guarded. I usually remove the equation from the simp set and add guarded versions to avoid this:

lemmas [simp del] = sum.simps

lemma sum_simps [simp]: "i > N ⟹ sum i N = 0" "i ≤ N ⟹ sum i N = i + sum (Suc i) N"
  by (auto simp: sum.simps)

proof of correctness for summation function with a counter

1 Answers