Kata

size e is a better bound for the number of operations. But it does not make the function more computationally efficient because the size of this bound is not important for computations: The same computations are performed for any correct bound.

but empirically it seems to run faster with 'size e'. (do you agree? eg for computing 2^32.)

why doesn't the number of stack frames scale with the first argument to 'pow_sqr_aux'? I am a neophyte and do not really understand lean internals yet.

Actually, you are right. I looked closer at the Lean definition of pow_sqr_aux and realized that it is not correct: It does not terminate when the third argument is 0 and keeps going on until the gas (the first argument) is exhausted. I am not going to fix it because there are no efficiency tests and I don't want to invalidate existing solutions. Other versions of this kata contain correct definitions of pow_sqr_aux which do not perform any extra operations even if the first argument is large.

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.

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.

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.

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.

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.

Thanks!

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.

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

Good job! Now you can try my latest kata which is somewhat similar to this one.