I believe this should be sorted, thanks.
Oops, sorry about this! I'll fix it now.
Please copy the content of Test Cases to Example Test Cases.
This comment is hidden because it contains spoiler information about the solution
I agree with monadius here. While kata based on the clever (ab)use of language features (such as the kata on embedding a stack-based language into Haskell mentioned in the Zulip chat) are most certainly welcome, there is a fine line between such clever kata and one that simply teaches how to break the system.
IMO the best course of action would be to unpublish this kata. If you discover loopholes within Codewars' Lean setup which can be (accidentally) bypassed and which cannot be defended against using a proper kata setup then feel free to report an issue on Codewars/codewars-runner-cli and we can see whether we can patch the loophole or otherwise find ways to detect such abuse automatically and mark them as cheats.
The description should clearly state that the goal of this kata is not to prove the given result but to pass tests by any means necessary. In general, it is a bad kata idea because it is possible to solve any Codewars kata by exploiting holes in test frameworks.
For what it's worth, I proposed this as a 7kyu kata :)
I also agree with the above comment that theorem proving kata can have different sorts of difficulty, but I think this particular one is mathematically fairly straightforward.
I agree with the statement of ipergenitsa above. Perhaps, for Coq and other theorem proving tools, it would be a good idea to differentiate between different aspects of the katas complexity (with a tag ?):
I think this particular problem would fall into the second category meaning that it is significantly harder for someone with a small background in mathematics. I personally struggled with problems of the third category (for example one using the very new feature of polymorphic universes in Coq).
Note that I may have missed the relevant tags and the respective meaning of 8kyu/7kyu etc (pointers are welcome ;) )
I am facing an issue while submitting the solution. Codewars Lean is not at the same state as my own editor when going through the proof. As a result it is not accepting my proof. I have checked that my proof works on my local machine (using Lean 3.8.0) and on the mathlib lean web editor (using Lean 3.9.0). Is the error being caused by CW's lean being at 3.7?
I agree that it should be 7kyu. But as I said, ranks can't be changed. It's 8kyu for non-beginners. ;-)
I would be glad to try this new area (theorem proving) as well as new (non-traditional) programming languages.
My opinion that 8kyu should be like the starting point, shouldn't it? But instead of simple stuff to get in touch with new ideas and approaches, I find hard tasks that forces me to read a book. I would like to see like step by step tasks. Otherwise this becomes very useless when the only people who can solve it the ones who worked with this before