One-off rank adjustments for overranked Coq Kata

[DonaldKellett]

As power users familiar with Coq know, many of the Coq Kata approved early when Coq was first introduced to Codewars were insanely overranked since someone wanted to reach 1 dan earlier and ended up abusing his Kata approval rights (almost) everyone was a n00b in theorem-proving back then and blindly ranked Coq Kata based on similar Kata in Haskell (which wasn't built for theorem-proving in the first place). Considering that such overrankings may have confused new Codewarriors specializing in Coq as to how the ranking system actually works on Codewars (i.e. 1 kyu is actually the difficult end and not the easy end) and I do not want the same to happen to Lean when it eventually gets added to Codewars (because by then we would have to translate a few simple Coq Kata into Lean as a demo before inviting in the "big players" to contribute Kata of their own), I would like to propose the following one-off rank adjustments to Coq Kata that I think are overranked:

Kata	Suggested Rank	Reason	Additional Remarks
Program Verification #1 - The sum of an arithmetic progression	6 kyu	Even though the use of division on natural numbers makes part of this Kata slightly awkward to work with, the Kata can be solved in a few lines using a direct induction, one or two lemmas on natural number division in the stdlib and a bit of automation using decision procedures which requires little thought.
Program Verification #2 - Fibonacci Numbers	6 kyu	The use of an auxiliary function means that the solver is required to manually generalize the induction hypothesis, but then the induction required after that is straightforward and the main theorem follows directly from this more general result.
This square is perfect	7 kyu	Although a beginner unaware of automation would have to perform a few tedious rewritings on the goal, the Kata can actually be trivially solved in 2-3 tactics with a standard decision procedure.
A + A = B + B so A = B? Prove it!	8 kyu	This can be solved directly using a decision procedure and even for beginners unaware of this, the induction is very standard and any beginner should be able to solve it after reading the first 2-5 chapters of Logical Foundations.
Google Interview	8 kyu	The induction is very standard and any beginner who has read the first 3 chapters of Logical Foundations should be able to solve it.
Magic is Commutative	7 kyu	Though perhaps not the most standard theorem-proving Kata, it can be solved with a few simple tactics.
DNE equivalent to PEM? Prove it!	7 kyu	Standard exercise on propositional logic that can be solved in a few lines; any beginner can solve it after reading the first 6 chapters of Logical Foundations	This Kata was originally authored in Haskell where it got its 2 kyu rank (which is still overranked but perhaps not so much so).
Transitivity	7 kyu	Perhaps not the most standard exercise but each individual proof can be completed using just a few simple tactics by fumbling around.
Introduction to bijection, cardinality and infinite sets	5 kyu	The bijections required in this Kata are rather standard and even though I found proving the final bijection in this Kata rather tricky back then (when I was still reading the final chapters of Logical Foundations), browsing existing solutions reveals that an experienced Coq user can complete each required proof under a few dozen standard tactics.
Simplifying conditional statements	6 kyu	Although this requires reading (almost) the entire volume of Logical Foundations, the proof is very short and simple, just under a dozen tactics with standard automation and a few dozen without.
Simplifying conditional statements, again	5 kyu	It is not difficult to find a counterexample informally, though translating it to a formal proof is a bit tedious (though not particularly difficult or challenging) and perhaps requires a few dozen tactics.
Yet another introduction to bisimulation, Chicken's style	6 kyu	This is just an introductory Kata to coinduction in Coq with no particular tricks required, and the solver should be able to complete the Kata by following the instructions in the Kata description.
Finding the maximal program	5 kyu	While the construction of the proof to this Kata is nontrivial, a major lemma is already provided in Logical Foundations which cuts down about half the required work.
EM implies LPO, LPO implies LLPO	5 kyu	The second proof in this Kata requires some clever reasoning on parity of numbers but the rest is straightforward once the solver gets the main idea.
Multiples of 3, you say?	5 kyu	The Kata requires the solver to extract out suitable lemmas (or work with an unwieldy nested induction) but otherwise is quite a standard problem typically found in a discrete math course.
A random fact about filtering	7 kyu	Easily completable by anyone who has read the first 5 chapters of Logical Foundations and experienced users can complete the entire proof under a dozen tactics.
Running around in circles, optimizing the Double Negation	6 kyu	The Kata is a bit tricky and requires extracting out a suitable lemma, but other than that, the rest is standard.
Exploring ways to evaluate and compile a trivial language	5 kyu	This Kata requires manually generalizing the induction hypothesis and extracting out a few lemmas but the rest is pretty standard.
Program Verification #4 - Exponentiation by Squaring	4 kyu	This Kata requires manually generalizing the induction hypothesis and it is not immediately obvious to the beginner (or even some intermediate Coq users) what generalization should be made; however, anyone having done a substantial portion of Verified Functional Algorithms (an undergraduate textbook) should have gained the skills to solve such Kata.
Rewriting on any binary equivalence relation	5 kyu	This Kata is an introduction to a Coq-specific language feature and requires some background reading but the actual theorems required in the Kata are quite standard and can be found in any discrete math course.

If anyone has alternative rank suggestions for any of the Kata listed above or would like to point out another overranked Kata not mentioned in the above table then feel free to chime in.

As for concerns about overloading Codewars' servers with these rank adjustments (because Codewars needs to recalculate the rank/honor of each Codewarrior affected, etc.), I don't think it will be a problem since there are only a few Coq completions per Kata (so the total number of Codewarriors affected is probably well under 100). Am I right @kazk?

Special mentions: @monadius, @Voileexperiments, @Bubbler-4, @dramforever

---

👍 reaction might help

[monadius]

I agree that ranks should be adjusted for many theorem proving kata. I have created a temporary wiki page which contains a table with suggested kata ranks. Anyone can add new ranks to this table (it now includes @DonaldKellett and my ranks).

[DonaldKellett]

@kazk Any plans on implementing the rank adjustments soon?

[kazk]

As for concerns about overloading Codewars' servers with these rank adjustments (because Codewars needs to recalculate the rank/honor of each Codewarrior affected, etc.), I don't think it will be a problem since there are only a few Coq completions per Kata (so the total number of Codewarriors affected is probably well under 100).

I don't think this will overload the servers. But I don't know if this will work as expected and adjust the honor points/language progress correctly, so I need to test and add the feature to do this if needed. If I remember correctly, it didn't work when the rank was being changed a while ago (but still overloaded the servers).

Any plans on implementing the rank adjustments soon?

I currently don't have a plan to do this "soon" since I have other tasks with higher priority. But I agree with the need of adjustments so I'll do it eventually.

Also, I'd like to see 2-3 more users to suggest the ranks on the wiki.

[Bubbler-4]

Added my ranking suggestion on the wiki page. I generally agree with monadius' rankings for the katas I remember of. (I've been away from theorem proving for months though.)

[kazk]

This Kata was originally authored in Haskell where it got its 2 kyu rank (which is still overranked but perhaps not so much so).

This is a known issue of having only one scale, but it might be better not to translate if the difficulty changes that significantly. So I'm not sure about changing this one to 7 kyu. It'll look out of place within Coq challenges, but that already happens with non-theorem proving kata (e.g., Python has many useful libraries that makes some tasks trivial).

[DonaldKellett]

Also, I'd like to see 2-3 more users to suggest the ranks on the wiki.

@dramforever @Voileexperiments Mind taking the time to add your rank suggestions to the wiki page for those Kata you have completed (just leave the corresponding entry blank if you have not solved it)?

This is a known issue of having only one scale, but it might be better not to translate if the difficulty changes that significantly.

I agree that submitting translations to a Kata with a huge difference in difficulty from the already supported languages is rarely a good idea. In order to prevent similar incidents from happening in the future, I have added a note at the beginning of the Kata Description for the remaining Haskell "theorem-proving" Kata, explicitly asking translators not to submit Coq/Idris/Agda translations.

So I'm not sure about changing this one to 7 kyu. It'll look out of place within Coq challenges, but that already happens with non-theorem proving kata (e.g., Python has many useful libraries that makes some tasks trivial).

That was precisely why I mentioned it in the "Additional Remarks" for that particular Kata.

But now that I think about it, perhaps it would still be better to downrank it to 6-8 kyu anyway and perhaps leave a note at the beginning of the Kata Description stating that the Kata is much harder in Haskell than in any of the proper theorem-proving languages.

The rationale for this is that Codewarriors will tend to choose the easy way (it's human nature!), so downranking the Kata to match the difficulty in Coq/Idris/Agda would prevent solvers from getting "easy points" in such a trivial Kata and I don't think many Codewarriors (given this warning) will be stupid enough to do it the hard way in Haskell anyway and perhaps waste hours on a 6-8 kyu Kata (if so, that is entirely their own fault and they shouldn't blame it on the ranking).

[ice1000]

I think it's a sensible thing to do. Though I believe 8kyu is too low, maybe increase the kyus by 1 each.

[kazk]

I realized I can probably just unapprove these kata, so you guys can change your rank assessments and approve them with adjusted rank.

I wasn't sure if adjustments to the honor points and the language progress work, but it seems to work since #2015 was caused by it.

I can unapprove some of these and see what happens.

[monadius]

@kazk You may start with my 3 kata 1, 2, 3.

[monadius]

@kazk Could you also make sure that the rating of this kata is computed correctly. It has 12 very satisfied and 5 somewhat satisfied votes but the rating is 63%.

[kazk]

@monadius Fixed the rating. Before the re-calculation, it was 12 "very", 5 "somewhat" and 63% of 23 (!?). Now it's 12 "very", 1 "somewhat" and 96% of 13.
I've also unapproved all 3.

[DonaldKellett]

I've just edited the wiki page to add a column indicating whether the Kata has been successfully re-ranked.

@kazk I am ready for the re-ranking anytime - feel free to un-approve whatever Coq Kata is in the wiki page as you see fit - just give me a heads-up when you do so.

@monadius As for the exact rankings used for the re-approval of the overranked Coq Kata mentioned, I suppose we'll just go with your suggested rankings since @Bubbler-4 's suggested rankings agree entirely with yours?