Additions to Haskell.Law.Bool

[HeinrichApfelmus]

This pull request adds additional properties to Haskell.Law.Bool.

This pull request tries to be systematic about these additions:

• Content:
  • We add properties for logical operations || and && that inspect the second argument, e.g. (x || True) ≡ True. These properties currently cannot be reached by computation, i.e. while (True || x) reduces to x, the expression (x || True) does not reduce further.
  • We add properties from the definition of Boolean Algebra.
• Style
  • Each property begins with -- and intersperses -- for visual separation between type ("interesting") and implementation ("don't care").
  • Each property puts the quantified variables on one line, and the conclusion on a separate line. This is also meant to help readability.
  • Each property is prefixed with prop-. Agda makes no distinction between programs and proofs, but when proving properties about Haskell programs, I find it conceptually helpful to distinguish target language (Haskell) from metalanguage (Agda), and prop- is a very clear visual separator.
    • When typing prop- into my editor (VSCodium), I get suggestions for completion, and these are now filtered to be metalanguage proofs rather than target programs.
    • The prop_ prefix is a convention used by QuickCheck. Using prop- in Agda2hs allows me to generate Haddock documentation like this:
    • More generally, when writing larger programs, we will eventually face the problem of discovering properties — Hoogle for prop-? I think that this prefix helps as well.

The content of these additions is highly useful for an axiomatization of Data.Set that I would like to contribute in a later pull request.

However, the main purpose of this pull request is to test maintainer opinions regarding the prop- prefix style, and the other style choices.

(In order to preserve backward-compatibility, I have chosen to not remove any now-redundant properties such as &&-sym. This can be done is a separate pull request if desired.)

[jespercockx]

Thank you for the PR! I think your reasoning for the naming and the layout makes perfect sense, I'm happy to go along with it.