Add Data.Nat.(Factorial/Combinatorics)

[MatthewDaggitt]

This PR results from me trying to refactor #1287. In this PR, the definition of _C_ (and the newly added _P_) are more efficient than the definition in the original PR. Firstly the operators no longer use Fin but instead requires you pass a proof that k ≤ n when using the properties. Secondly it no longer evaluates _C_ recursively which took exponential time. I haven't made my way all the way up to the binomial theorem yet, but I thought this was a good point to merge in.

@uzytkownik any feedback you have would be more than welcome!

One niggle that I did encounter is that the current dependency cycles between Data.Nat.Divisibility and Data.Nat.DivMod make the proof m/n/o≡m/[n*o] seriously hard to place, in that it currently requires proofs from both of them and therefore can't live in either. I can't immediately see how to fix it without either adding in a load more nearly empty modules or carrying out the planned reorganisation of the files which will occur in #921. Given that, I've added the proof as a private definition in the new files and will open a new issue to get it fixed in v2.0.

[JacquesCarette]

That definition of binomial is still pretty slow. See the 2nd answer to https://math.stackexchange.com/questions/202554/how-do-i-compute-binomial-coefficients-efficiently for good ways to compute it.

[MatthewDaggitt]

That definition of binomial is still pretty slow. See the 2nd answer to https://math.stackexchange.com/questions/202554/how-do-i-compute-binomial-coefficients-efficiently for good ways to compute it.

Hmm, yes I was foolishly only counting number of operations, not the magnitude of the numbers involved. I'll see if I can tweak it.

[subttle]

Not sure if this is of any direct help to you (I haven't looked closely at your code yet) but perhaps it is worth mentioning that the factorial function can be written as a paramorphism for good efficiency.

See slide 58/106.

fact :: Integer -> Integer
fact = para alg where
  alg Zero = 1
  alg (Succ (f, n)) = f * (n + 1)

[MatthewDaggitt]

@JacquesCarette I'm afraid updating the implementation to be more efficient results in far more work changing the proofs than I'm currently willing to do. I think that an inefficient implementation is better than no implementation at all so I propose to merge it in.

I've brought the code up to date and added a link to the better implementation in the comments.

[JacquesCarette]

For the record: I agree that an (inefficient) implementation is better than no implementation. That so many proofs break is a symptom of something discussed already: many fragile proofs that rely on implementation details, rather than being more conceptual. Something for a later day.