Consider this problem appearing in Codeforces (rated 1500):
There are n boxers, the weight of the i-th boxer is ai. Each of them can change the weight by no more than 1 before the competition (the weight cannot become equal to zero, that is, it must remain positive). Weight is always an integer number.
It is necessary to choose the largest boxing team in terms of the number of people, that all the boxers' weights in the team are different (i.e. unique).
Write a program that for given current values ai will find the maximum possible number of boxers in a team.
It is possible that after some change the weight of some boxer is 150001 (but no more).
Input :The first line contains an integer n (1≤n≤150000) — the number of boxers. The next line contains n integers a1,a2,…,an, where ai (1≤ai≤150000) is the weight of the i-th boxer.
Output :Print a single integer — the maximum possible number of people in a team.
Here is the code I implemented which was accepted by the Codeforces as a correct submission (Python 3.7):
n=int(input())
inputlist=list(map(int, input().split()))
inputlist.sort()
boxerset=set()
for i in inputlist:
if i-1 not in boxerset and i!=1:
boxerset.add(i-1)
elif i not in boxerset:
boxerset.add(i)
elif i+1 not in boxerset:
boxerset.add(i+1)
else:
continue
print(len(boxerset))
However, I am not able to rigorously prove that this algorithm necessarily give the correct answer. For example, when inputlist is [1, 1, 1, 2, 2, 5 , 8], both [1, 2, 3, 4, 7, 8](my algorithm) and [1, 2, 3, 6, 7, 8] is the correct output boxerset, although the answer for both the cases comes out to be 6.
My question is this:
How can I prove my algorithm is correct? How will my proof work to show that out of all possible legal selections of boxers, the selection by my algorithm has the maximum amount of boxers (that is how do I show that my there exists no other selection for which the number of boxers can be greater than the selection done by my algorithm)?
I have tried proof by contradiction but to no avail (although I think the proof has to have the natural structure of a proof by contradiction).
David Eisenstat's last sentence on the second paragraph of his answer "Hence the dynamic program should track the maximum team size for each fighting weight bound" has inspired me to an alternate solution. I use induction:
Assume that while iterating through the loop, the maximum fighting weight of the fighter selected is k.
The inductive assumption is that this subsequence consists of the maximum team size for weight bound k.
As the inductive step, when the next iterations add the higher fighting weight, this is obviously the maximum team size with weight bound k+1.
To see this, assume this is not the case. Then there exists a subsequence with the more team size than the one created from our algorithm. Remove k+1 fighter from this list. Then this list should be the largest subsequence of weight bound k, which leads to contradiction from the inductive hypothesis. Hence the correctness of the algorithm is proved.
The only case which is not included is where there is only 1 possible fighter in the boxerlist. This case is trivial and hence the proof is complete.