Add notes about code formatting and style

STYLE.md

@@ -0,0 +1,139 @@
+These are a few notes on conventions, style and formatting used in
+this library.
+
+# 1. Applying these notes
+This library contains many different conventions mixed
+together. So changing the style all at once would be a lot of work.
+Instead it suffices that all new changes adhere to these notes.
+
+The formatting is mostly based on what is easy to achieve with
+ProofGeneral without further configuration.
+
+# 2. File Structure
+Within ZornsLemma, the only files which shall develop any theory about
+`Finite` and `FiniteT` shall be `Finite_sets` for the former and
+`FiniteTypes` for the latter. This is to prevent circular
+dependencies.
+
+The folder `Cardinals` shall only contain facts which are independent of
+any fixed type or subset. I.e. no properties of [nat] or uncountable sets.
+Those shall be put in other files. But combinatorics of sets (existence of
+injections, surjections, bijections/invertible maps) is fine.
+This is again to prevent circular dependencies.
+
+# 3. Indentation
+Use two spaces per indentation level.
+A `Section` or `Module` causes a new indentation level in most cases. If the
+`Section` or `Module` takes up the majority of the file, maybe don't use a new
+indentation level, so the text doesn't shift too far to the right.
+
+The block of Ltac code of a proof (between `Proof.` and `Qed.` or `Defined.`)
+is on a new indentation level. (default in ProofGeneral) Braces and bullets
+always cause a new indentation level.
+
+# 4. Imports
+Prefer `Require Import` over `Require Export`.
+
+Using `Require Export` the dependenices between files are kept
+invisible, which makes it harder to detect which import causes a given
+definition or notation to be loaded. Also, if circular dependencies
+would arise, it can be hard to find out how it is caused.
+
+Formatting of imports.
+Prefer
+```coq
+From Coq Require Import
+  ClassicalChoice
+  Description
+  Program.Subset.
+From ZornsLemma Require Import
+  DecidableDec
+  EnsemblesImplicit
+  Families
+  FunctionProperties
+  Image
+  InverseImage
+  Powerset_facts
+  Proj1SigInjective.
+(* load [RelationClasses] last to override [Relations_1] *)
+From Coq Require Import RelationClasses.
+```
+to all previous styles. It is defined by
+* A command has the form `From XX Require Import/Export YY.` to give
+  the full path to each imported file.  This prevents ambiguities. For
+  example some files have identical names to files in the standard
+  library and if the `Require` isn't qualified, then Coq might get
+  confused and load the wrong file.
+* Start with imports from `Coq`, then other libraries if necessary,
+  then imports from the current library. Put `Require Import` before
+  `Require Export`.
+  This allows the definitions of the current library to overwrite
+  other libraries.
+  If for some reason a file needs to overwrite previous imports, put
+  it last.
+* If multiple files from the same library are imported, use separate
+  lines for each file. Indent by two spaces and order the files
+  alphabetically.
+  This creates simpler diffs when adding/removing files than when
+  multiple files are on a single line. The merge conflicts can be very
+  complicated.
+
+# 5. Proof formatting
+Proofs begin with `Proof.` on the same indentation as the `Lemma` (or
+similar) statement. The Ltac commands of the proof start on a new line
+and are indented by two spaces (as done automatically by ProofGeneral).
+
+## Use bullets and braces
+Always use bullets, braces or explicit goal selectors (like `2:` or `all:`)
+when multiple goals are created. Insert `Set Default Goal Selector "!".` into
+the Coq-file or `-arg -set -arg "'Default Goal Selector=!'"` into the
+`_CoqProject` file to check whether some places have been missed.
+
+In general, use bullets if the goals are of equal "importance" and braces for
+"intermediate goals". Consider how you would order and structure the branches
+of a proof in writing (on paper).
+
+Always use braces after `assert` or when any tactic causes "intermediate
+goals". Like `destruct` of a term like `A -> exists x, P x`.
+
+Generally use bullets after a `split` on a goal like `_ /\ _` or after
+`destruct` of a hypothesis like `_ \/ _` or `option _`. But if one of the two
+branches is much easier to solve (e.g., in less than 5 tactics) and the other goal
+needs more involved work (more lemmas etc.) then solve the easier goal first
+using a brace (use `2: {` if necessary, to reorder goals).
+This often happens when in a text we would say "if the space is empty, the
+statement is trivial".
+
+On a new branch (be it bullet or brace) it can be useful to add a comment
+explaining which case of a case distinction or which constructor of an
+induction gets treated. This especially helps when the proof has to be
+restructured when constructors are added. The comment takes the place
+of the first tactic.
+
+Reason: Make proofs more readable. Let the formatting of the proof reflect its
+structure.
+
+### Formatting braces
+Examples:
+```coq
+Goal False.
+assert (False).
+{ admit. }
+idtac.
+assert (False).
+{ idtac.
+  idtac.
+  admit.
+}
+assert (False).
+{ (* comment here *)
+  idtac.
+  idtac.
+  admit.
+}
+destruct (andb A B).
+2: {
+  idtac.
+}
+idtac.
+```