The definition is monstrous when unfolded, but luckily Lean's rewrite matches the huge expressions masterfully and does unification automatically so that the induction hypothesis is applied correctly, as in my solution (rw ih): https://www.codewars.com/kumite/5f2e30269de164002a276bd0?sel=5f2e303cf51db50010b60b36

Using gas instead of well-founded recursion is fine and preserves the original intent of the problem. But using recursors (nat.rec_on, etc.) directly is not idiomatic in Lean (or in any other theorem prover as far as I know). Using the equation compiler even for structural recursion makes a difference in Lean because it causes equational lemmas to be generated.

Approved - I think I found a way to keep the Coq snippets from the original description.

Thanks for taking the time to translate my Kata. I see that you have replaced the Coq snippets with Lean ones, would you mind keeping them instead (and have your Lean snippets next to the Coq ones)? That way, Coq solvers can see the Coq snippets (only) and likewise for Lean, cheers :-D

Same here. I feel like I should have looked at the language features more closely before getting started. Something should have jumped at me

I'm porting this Kata to Lean. How do I add the axiom of choice to the forbidden axioms?

Why deceitful?

Thanks!

I don't want to change definitions in this kata but I'm going to update my other kata and use well-founded recursion in Lean there.

I don't want to insist too much. I'd just add that rather than offerring this alternative because there's a different way of doing things, I'd say that if this is the best way of doing things in Idris, it is not in Lean. If learning Idris entails learning this approach, it is a more esoteric approach in Lean because there exists simpler ways.

I would also offer that, if the kata had first been authored in Lean, it might have ended up equally awkward for Idris users to solve the translation, if a faithful translation does indeed exist. This being said, I am new to the CodeWars community so i don't want to dictate priorities.

A citation from Codewars wiki: "A translation is essentially just a "port" of the original kata to a new language. Every aspect of the original kata should be retained." It is not enforced but it is a good practice to keep all translations consistent. I consider the original definition to be important so I don't want to change the Lean version. The original intention of the kata is the following: Verify that the given program is correct. It is wrong to change the program in Lean only because there is another way to write the same program.

The issue here is that it means the definition is in Lean more complicated than necessary and it is not idiomatic. It might feel more natural to Idris users but not to Lean users. That's why I would suggest we change the Lean version.

It is definitely possible. But the original version of this kata is done in Idris where the current definition is much simpler than a definition based on well-founded recursion. All translations faithfully preserved the original definition.

Can't we use equations and well-founded recursion to define pow_sqr_aux?