is this loop invariant and post condition correct?

I was trying to write a loop invariant and post condition for this code:

sum = 0;
for (i = 0; i < 10; ++i)
  ++sum;

sum = 10 is the obvious post condition here. But a friend told me that i = sum is also a loop invariant and sum = 12 is also a post condition. I checked the following:

• loop invariant is initially true: that's true for i = sum since both are 0 initially
• loop invariant is preserved: assume i < 10 and i = sum then after one iteration it's still true that ++i = ++sum
• loop invariant implies post condition: assume i >= 10 and i = sum then sum = 12 is also true

But obviously sum doesn't equal to 12 here. So what's wrong with my reasoning here?

Take a slightly different invariant i == sum && i <= 10. Together with i >= 10 you get then i = sum = 10.

Btw. in your original reasoning you cannot conclude that sum = 12 is true but only that sum >= 10. The latter is correct, just not strong enough to prove the desired result.