I'm interested in a variation of the argument that stablishes:
"(∑ i=1..k . i) = k*(k+1) div 2"
We know this follows from a simple induction but the intution is a bit different. A way to see this formula is that if you sum the extremes of the sequence of numbers 1..k you get
1+k = 2 + (k-1) = ...
and then you just multiply the right number of times to get the complete sum.
I would like to reproduce this argument to show the following inequality:
"(∑n = 1..k - 1. cmod (f (int n))) ≤ 2 * (∑n ≤ k div 2. cmod (f (int n)))"
Here I know that cmod (f (int k - n)) = cmod (cnj (f n)) for every n.
Do you see an elegant way of proving this in Isabelle?
The trick to do this proof in an elegant way is to realise that ∑i=1..k. i is the same as ∑i=1..k. k + 1 - i and then adding that to the original sum so that the i cancels. This is a simple re-indexing argument:
lemma "(∑i=1..k. i :: nat) = k * (k + 1) div 2"
proof -
have "(∑i=1..k. i) = (∑i=1..k. k + 1 - i)"
by (rule sum.reindex_bij_witness[of _ "λi. k + 1 - i" "λi. k + 1 - i"]) auto
hence "2 * (∑i=1..k. i) = (∑i=1..k. i) + (∑i=1..k. k + 1 - i)"
by simp
also have "… = k * (k + 1)"
by (simp add: sum.distrib [symmetric])
finally show ?thesis by simp
qed
For the other thing you mentioned, I think that the best way to do this is to first split the sum into the elements less that k div 2 and the rest. Then you can reindex the second sum similarly to the one above. Then the inequality part comes in because you might have one extra leftover element ‘in the middle’ if k is odd and you have to throw that away.
Brief sketch of the important part of the proof:
lemma
assumes "⋀i. f i ≥ 0"
shows "(∑i=1..<k. f (i::nat) :: real) = T"
proof -
(* Separate summation domain into two disjoint parts *)
have "(∑i=1..<k. f i) = (∑i∈{1..k div 2}∪{k div 2<..<k}. f i)"
by (intro sum.cong) auto
(* Pull sum apart *)
also have "… = (∑i∈{1..k div 2}. f i) + (∑i∈{k div 2<..<k}. f i)"
by (subst sum.union_disjoint) auto
(* Reindex the second sum *)
also have "(∑i∈{k div 2<..<k}. f i) = (∑i∈{1..<k - k div 2}. f (k - i))"
by (rule sum.reindex_bij_witness[of _ "λi. k - i" "λi. k - i"]) auto
(* Throw away the element in the middle if k is odd *)
also have "… ≤ (∑i∈{1..k div 2}. f (k - i))"
using assms by (intro sum_mono2) auto
finally have "(∑i=1..<k. f i) ≤ (∑i=1..k div 2. f i + f (k - i))"
by (simp add: sum.distrib)
Figuring out how to do these sum manipulations idiomatically in Isabelle takes some experience. sum.reindex_bij_witness is a very useful rule (as you can see). Things like sum.mono_neutral_left/right can also help a lot.