From 2a23da23d0467e600029130bb4cccb33375b0a22 Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Sun, 8 Oct 2023 11:22:59 +0200
Subject: [PATCH] Incorporate the notes from #19

The notes added in this commit were previously published at
https://gist.github.com/Columbus240/a1ece869fd4df72d1b056767075d8eb5
---
 STYLE.md | 77 ++++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 72 insertions(+), 5 deletions(-)

diff --git a/STYLE.md b/STYLE.md
index d6423780..c623168e 100644
--- a/STYLE.md
+++ b/STYLE.md
@@ -9,7 +9,7 @@ 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. Structure
+# 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
@@ -21,7 +21,17 @@ 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. Imports
+# 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
@@ -50,8 +60,10 @@ 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.
+  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`.
@@ -66,7 +78,62 @@ to all previous styles. It is defined by
   multiple files are on a single line. The merge conflicts can be very
   complicated.
 
-# 4. Proof formatting
+# 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.
+```