I think I have you beat on that now lol

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.

Nice Kata, thanks! My approach is by far the most convoluted to date (-X

If all goes well, the Kata should be approvable after 1-2 more satisfaction and ranking votes. Looking forward to more Coq Kata authored by you ;-)

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.)

Please use the Codewars Coq plugin for tests:

Require Import Preloaded.
Require Solution.
From CW Require Import Loader.

CWGroup "nnf_of_expr_sound".
  CWTest "nnf_of_expr type".
    CWAssert Solution.nnf_of_expr_sound : 
      (forall e v, eval_nnf (Solution.nnf_of_expr e) v = eval e v).
        
  CWTest "nnf_of_expr assumptions".
    CWAssert Solution.nnf_of_expr_sound Assumes.
CWEndGroup.

Thanks for the suggestion, I'll keep that in mind when authoring future Kata. The current efficient implementation is a direct translation of my JavaScript solution to the original Kata which did not take formalization considerations into account.

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.)

Actual tests:

The reference eval_nnf was not found in the current environment.
File "./SolutionTest.v", line 4, characters 4-12