Hey all, I've noticed that although I can get AC on problems, I am utterly unable to formalize my intuition into a correctness proof.
For example, consider my AC solution to 1672C.
In my head, my justification for my approach was something like "after the $$$i$$$-th iteration, we have either performed an operation on it or not. If we performed an operation, $$$a_{i - 1} = a_i$$$, and this is the only index in $$$1, 2, \ldots, i - 1$$$ where this is true". This helped me realize that at the conclusion of the algorithm, we would have an array of equality $$$<=1$$$ as desired. However, despite my best efforts, I just couldn't show that my code did so in the minimal number of moves.
Now, this may be normal for a CP'er who's still in high school, but, as a CS graduate who's taken a number of math courses at university, I'm a little embarrassed that I'm having trouble proving the correctness of problems that are relatively simple (i.e. rated $$$[800, 1100]$$$).
To be explicit, I've taken proof-based classes in:
- Discrete mathematics
- Combinatorics
- Graph theory
- Number theory
- Algorithms
so I know what rigorous math looks like, but the skillset just hasn't transferred over to correctness proofs. In my algorithms class, we spent a lot of time proving time complexities for standard algorithms like merge sort, but we never really focused on correctness.
I've looked at CLRS as well, but the exercises are formulated in a way that does the hard work for you (i.e. prove that this lemma is true vs. what is the lemma that you should prove to show correctness). Also, CLRS focuses on proving loop invariants via induction, but this isn't that useful for analyzing greedy algorithms, which dominate the problems I've been working on.
Has anyone successfully trained themselves out of this?
Is there a math book or a CSES-style problem set focused on correctness proofs that I could work my way through to get better?
Why do you want to formalize your intuition?
It's not a math competition, it's a programming competition, as long as you've a strong intuitive sense that your algorithm is correct it's more than enough, then you can test it out with few small samples or if you still want "proof" you can try stress testing.
Intuition, no matter how strong, often fails though.
This is especially true for problems that seem greedy, but are actually not.
I disagree, I think it's very good that the author wants to prove their solutions!
For this specific problem, I don't have time to read your solution unfortunately, but I believe the intended solution might be easier to prove. Just like with how finding a shorter implementation is good, I think finding an easier-to-prove solution is good.
Here is my proof: let $$$l$$$ be the smallest integer such that $$$a_l = a_{l + 1}$$$. Let $$$r$$$ be the largest integer such that $$$a_r = a_{r + 1}$$$. If neither integer exists, then the answer is obviously $$$0$$$. Consider how the value of $$$r - l$$$ changes when we perform an operation on the array.
It's easy to see that we can perform zero operations iff $$$r - l = 0$$$. If $$$0 < r - l \leq 2$$$, then one operation is possible, which is optimal from the previous statement. Otherwise, we can prove using some casework that the value of $$$r - l$$$ can decrease by at most $$$1$$$, and to be really formal, I guess the solution follows from induction on $$$r - l$$$.
This type of proof is quite common — it's also used in proving stuff like "what is the minimum number of swaps required to sort a permutation"?
As for how to get better at them, I guess just like with problems, just do more and recognize some patterns.
BTW for proving greedys, it almost always uses an exchange argument.
Your thinking is the reason for many people to be stuck in low ranks.
Oh boi, seems like people got the wrong idea by what I meant.
Do you "formally" prove your solutions before submitting in a contest?
I didn't say anything against proving, I was talking about the rigorousness of a proof which seemed like what the OP intended, if you're sketching up a rigorous mathematical proof for every solution you're submitting then you're just wasting time(and more so if it's a live contest).
What I meant by strong intuition is that when you see a problem you've certain ideas on how to go about solving it, and you work on some ideas which makes sense and is reasonable. Your intuition develops the more problems you solve.
Yes, most often I do.
That's the reason I didn't get AC (note: AC isn't solving) in F1 from last global, I had a construction that made intuitive sense but I had no fucking idea about why it'd work, so I didn't submit.
Well you might be wasting time by implementing a solution with wrong intuition. Personally I don't formally prove every single details, but I generally prefer to at least have a proof sketch (that can be turned into a complete rigorous proof without much difficulty) before submitting a solution.
Was there anything in particular (beyond just solving more problems) that helped you improve this skill?
If I were to point out things that helped me outside of solving problems and reading editorials/comment sections, the most important for me were:
Talking to other people about problems (online and offline). Convincing another person of your idea is a good exercise for trying to expose your ideas in a rational (less intuitive) way. It also goes both ways because I think it's easier to be objective about other people's ideas, thus you're less likely to just think "this makes sense" and leave the problem at that point.
A specific graph theory class I took in the math department in my university. Since the class was kinda small, interaction in this specific class was great and it developed my "formal logic" skills by a lot. Needless to say, I didn't take this class just to pass it, I took it thinking about how it could be good for me as a CP competitor.
...I generally prefer to at least have a proof sketch (that can be turned into a complete rigorous proof without much difficulty) before submitting a solution.
That's what I meant, exactly. (Guess my wording wasn't better, welp no more commenting on cf ig where people just downvote anything which goes against their perceived reality)
Apparently, it seems like what I referred to as "strong intuition" is an actual thing.
I thought that's exactly why the downvote button existed
Yes sir, I do.
Pranav Sriram's book is good. Unfortunately, too difficult for me.
Second this. Great book
I also have big problems with proofing my solutions(
Your intuition must be very strong.