What's the motivation behind this kata? I don't understand why we're proving equality of a bunch of proof terms.

• The initial body cannot be reduced.
• Only match-reduction could be enabled by replacing n with a concrete value (e.g. S (S O)), but n is not being matched, so still no reduction is available. So, e.g., strange 0 and strange 1 are obviously not alpha-convertible. (Try using "Compute strange 0" to see.)
• But replacing u with tt does enable match-reduction, yielding (fun _ => tt) n, followed by beta-reduction, to give just tt.

I loved the simplicity of this kata. Very cool.

Thanks, that's very helpful. (FYI, the "Insert Example" kata still uses the old-style tests, which is why this kata originally used that style.)

It's not a problem for the proof, but isn't it a bit odd that the optimized version uses minus? I would have expected something more along the lines of

Fixpoint parts_sums_efficient' (xs : list Z) : Z * list Z :=
  match xs with
  | nil => (0, [0])
  | x :: xs' =>
    let (acc, ys') := parts_sums_efficient' xs' in
    let acc' := x + acc in
    (acc', acc' :: ys')
  end.

Definition parts_sums_efficient (xs : list Z) : list Z :=
  snd (parts_sums_efficient' xs).

This way the same implementation can be used for types that support some form of addition but not subtraction. (e.g. You could compute all suffixes of a list.) It also uses fewer arithmetic operations because of not making the initial call to sum.

Thanks! It should be fixed now. (The reason it slipped through is that I didn't realize that clicking "Validate Solution" only checks whichever test tab is currently selected.)