Implementing `IsLawfulNum` as part of Issue #108

[pmbittner]

This pull-request adds the laws for the Num typeclass in Haskell as part of issue #108.

Progress:

• [x] formalized the laws for Num typeclass
• [x] Nat instance
• [x] Int instance
• [x] Integer instance
• [x] Word instance
• ~Double instance~

There was one law we cannot formalize yet, which is fromInteger (toInteger i) == i because there is no toInteger function available yet. I documented this law as missing.

For the Nat instance, I mostly copied code from the Agda standard library for comparability, consistency, and also because it is easy :sweat_smile:.

For Integer I had to come up with new proofs because the definitions for this type are slightly different from those in the standard library. I oriented on the proofs from the standard library where possible though. Also I tried to favor equational reasoning in favor of rewrite for better readability.

Arithmetics of Word is mostly relying on arithmetics of Nat and arithmetics of Int is defined solely in terms of arithmetics on Word. I hence opted to reuse the laws from the other instances, respectively. In fact, reducing the arithmetics for a Num type in terms of another Num instance is feasible as long as this reduction is homomorphic.

To formalize this observation, I added definitions for homomorphisms, embeddings, as well as some other common predicates in a new module Haskell.Prim.Function with respective proofs in Haskell.Law.Function. I thought that such definitions might be useful in other contexts as well, if desired. Using these definitions, we can then define the circumstances under which we may conclude an ILawfulNum instance from another one.

The question remains whether such abstractions are desired. On the one hand, these are quite common concepts. On the other hand, they introduce another layer of indirection and abstractions, making some of the proofs harder to comprehend. Also, should we reuse the definitions such as Associative, Commutative, and so on in the definition of IsLawfulNum or should we inline those (as it currently is) for readability?

Moreover, I had to introduce six new axioms to prove lawfulness of Word, all of which are stated in lib/Haskell/Law/Num/Word.agda. I documented the new axioms and explained why they should be reasonable. It would be good if these could be reviewed. I am not 100% sure that they are correct and minimal.

Also, the Double instance cannot be proven as of now. It is solely based on primitive functions for which no axioms exist yet. So I left that out for now.

[pmbittner]

This PR is now ready to review.