feat(doc/lean/library_style.org,README.md): add library style conventions

README.md

@@ -72,6 +72,7 @@ Miscellaneous
 - [Testing and Code Coverage](doc/make/coverage.md)
 - Building Doxygen Documentation: `doxygen src/Doxyfile`
 - [Coding Style](doc/coding_style.md)
-- [Git Commit Convention](doc/commit_convention.md)
+- [Library Style Conventions](doc/lean/library_style.org)
+- [Git Commit Conventions](doc/commit_convention.md)
 - [Automatic Builds](doc/make/travis.md)
 - [Syntax Highlight Lean Code in LaTeX](doc/syntax_highlight_in_latex.md)

doc/lean/library_style.org

@@ -0,0 +1,321 @@
+#+Title: Library Style Guidelines
+#+Author: [[http://www.andrew.cmu.edu/user/avigad][Jeremy Avigad]]
+
+Library Style Guidelines
+========================
+
+Files in the Lean library generally adhere to the following guidelines
+and conventions. Having a uniform style makes it easier to browse the
+library and read the contents, but these are meant to be guidelines
+rather than rigid rules.
+
+Identifiers and theorem names
+-----------------------------
+
+We generally use lower case with underscores for theorem names and
+definitions. Sometimes upper case is used for bundled structures, such
+as =Group=. In that case, use CamelCase for compound names, such as
+=AbelianGroup=.
+
+We adopt the following naming guidelines to make it easier for users
+to guess the name of a theorem or find it using tab completion. Common
+"axiomatic" properties of an operation like conjunction or
+multiplication are put in a namespace that begins with the name of the
+operation:
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check and.comm
+check mul.comm
+check and.assoc
+check mul.assoc
+check mul.left_cancel -- multiplication is left cancelative
+#+END_SRC
+In particular, this includes =intro= and =elim= operations for logical
+connectives, and properties of relations:
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check and.intro
+check and.elim
+check or.intro_left
+check or.intro_right
+check or.elim
+
+check eq.refl
+check eq.symm
+check eq.trans
+#+END_SRC
+
+For the most part, however, we rely on descriptive names. Often the
+name of theorem simply describes the conclusion:
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check succ_ne_zero
+check mul_zero
+check mul_one
+check sub_add_eq_add_sub
+check le_iff_lt_or_eq
+#+END_SRC
+If only a prefix of the description is enough to convey the meaning,
+the name may be made even shorter:
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check neg_neg
+check pred_succ
+#+END_SRC
+When an operation is written as infix, the theorem names follow
+suit. For example, we write =neg_mul_neg= rather than =mul_neg_neg= to
+describe the patter =-a * -b=. 
+
+Sometimes, to disambiguate the name of theorem or better convey the
+intended reference, it is necessary to describe some of the
+hypotheses. The word "of" is used to separate these hypotheses:
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check lt_of_succ_le
+check lt_of_not_le
+check lt_of_le_of_ne
+check add_lt_add_of_lt_of_le
+#+END_SRC
+Sometimes abbreviations or alternative descriptions are easier to work
+with. For example, we use =pos=, =neg=, =nonpos=, =nonneg= rather than
+=zero_lt=, =lt_zero=, =le_zero=, and =zero_le=.
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check mul_pos
+check mul_nonpos_of_nonneg_of_nonpos
+check add_lt_of_lt_of_nonpos
+check add_lt_of_nonpos_of_lt
+-- END
+#+END_SRC
+
+These conventions are not perfect. They cannot distinguish compound
+expressions up to associativity, or repeated occurrences in a
+pattern. For that, we make do as best we can. For example, =a + b - b
+= a= could be named either =add_sub_self= or =add_sub_cancel=. 
+
+Sometimes the word "left" or "right" is helpful to describe variants
+of a theorem.
+#+BEGIN_SRC lean
+import standard algebra.ordered_ring
+open nat algebra
+
+check add_le_add_left
+check add_le_add_right
+check le_of_mul_le_mul_left
+check le_of_mul_le_mul_right
+#+END_SRC
+
+Line length
+-----------
+
+Lines should not be longer than 100 characters. This makes files
+easier to read, especially on a small screen or in a small window.
+
+Header and imports
+------------------
+
+The file header should contain copyright information, a list of all
+the authors who have worked on the file, and a description of the
+contents. Do all =import=s right after the header, without a line
+break. You can also open namespaces in the same block.
+
+#+BEGIN_SRC lean
+/-
+Copyright (c) 2015 Joe Cool. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joe Cool.
+
+A theory of everything.
+-/
+import data.nat algebra.group
+open nat eq.ops
+#+END_SRC
+
+Structuring definitions and theorems
+------------------------------------
+
+Use spaces around ":" and ":=". Put them before a line break rather
+than at the beginning of the next line.
+
+Use two spaces to indent. You can use an extra indent when a long line
+forces a break to suggest the the break is artificial rather than
+structural, as in the statement of theorem:
+
+#+BEGIN_SRC lean
+theorem two_step_induction_on {P : nat → Bool} (a : nat) (H1 : P 0) (H2 : P (succ 0))
+    (H3 : ∀ (n : nat) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
+sorry
+#+END_SRC
+
+If you want to indent to make parameters line up, that is o.k. too:
+#+BEGIN_SRC lean
+theorem two_step_induction_on {P : nat → Bool} (a : nat) (H1 : P 0) (H2 : P (succ 0))
+                              (H3 : ∀ (n : nat) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) :
+  P a :=
+sorry
+#+END_SRC
+
+After stating the theorem, we generally do not indent the first line
+of a proof, so that the proof is "flush left" in the file.
+#+BEGIN_SRC lean
+theorem nat_case {P : nat → Bool} (n : nat) (H1: P 0) (H2 : ∀m, P (succ m)) : P n := 
+induction_on n H1 (take m IH, H2 m)
+#+END_SRC
+
+When a proof rule takes multiple arguments, it is sometimes clearer, and often
+necessary, to put some of the arguments on subsequent lines. In that case,
+indent each argument.
+#+BEGIN_SRC lean
+theorem nat_discriminate {B : Bool} {n : nat} (H1: n = 0 → B)
+    (H2 : ∀m, n = succ m → B) : B :=
+or_elim (zero_or_succ n)
+  (take H3 : n = zero, H1 H3)
+  (take H3 : n = succ (pred n), H2 (pred n) H3)
+#+END_SRC
+Don't orphan parentheses; keep them with their arguments.
+
+Here is a longer example.
+#+BEGIN_SRC lean
+theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
+list.induction_on l
+  (take H : x ∈ [], false.elim (iff.elim_left !mem_nil_iff H))
+  (take y l,
+    assume IH : x ∈ l → ∃s t : list T, l = s ++ (x::t),
+    assume H : x ∈ y::l,
+    or.elim (eq_or_mem_of_mem_cons H)
+      (assume H1 : x = y,
+        exists.intro [] (!exists.intro (H1 ▸ rfl)))
+      (assume H1 : x ∈ l,
+        obtain s (H2 : ∃t : list T, l = s ++ (x::t)), from IH H1,
+        obtain t (H3 : l = s ++ (x::t)), from H2,
+        have H4 : y :: l = (y::s) ++ (x::t), from H3 ▸ rfl,
+        !exists.intro (!exists.intro H4)))
+#+END_SRC
+
+A short definition can be written on a single line:
+#+BEGIN_SRC lean
+definition square (x : nat) : nat := x * x
+#+END_SRC
+For longer definitions, use conventions like those for theorems.
+
+A "have" / "from" pair can be put on the same line.
+#+BEGIN_SRC lean
+have H2 : n ≠ succ k, from subst (ne_symm (succ_ne_zero k)) (symm H),
+[...]
+#+END_SRC
+You can also put it on the next line, if the justification is long.
+#+BEGIN_SRC lean
+have H2 : n ≠ succ k,
+  from subst (ne_symm (succ_ne_zero k)) (symm H),
+[...]
+#+END_SRC
+If the justification takes more than a single line, keep the "from" on the same
+line as the "have", and then begin the justification indented on the next line.
+#+BEGIN_SRC lean
+have n ≠ succ k, from
+  not_intro
+    (take H4 : n = succ k,
+      have H5 : succ l = succ k, from trans (symm H) H4,
+      have H6 : l = k, from succ_inj H5,
+      absurd H6 H2)))),
+[...]
+#+END_SRC
+
+When the arguments themselves are long enough to require line breaks, use
+an additional indent for every line after the first, as in the following
+example:
+#+BEGIN_SRC lean
+theorem add_right_inj {n m k : nat} : n + m = n + k → m = k :=
+induction_on n
+  (take H : 0 + m = 0 + k,
+    calc
+        m = 0 + m : symm (add_zero_left m)
+      ... = 0 + k : H
+      ... = k     : add_zero_left k)
+  (take (n : nat) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
+    have H2 : succ (n + m) = succ (n + k), from
+      calc
+        succ (n + m) = succ n + m   : symm (add_succ_left n m)
+                 ... = succ n + k   : H
+                 ... = succ (n + k) : add_succ_left n k,
+    have H3 : n + m = n + k, from succ_inj H2,
+    IH H3)
+#+END_SRC lean
+
+Binders
+-------
+
+Use a space after binders:
+or this:
+#+BEGIN_SRC lean
+example : ∀ X : Type, ∀ x : X, ∃ y, (λ u, u) x = y
+#+END_SRC
+
+Calculations
+------------
+
+There is some flexibility in how you write calculational proofs. In
+general, it looks nice when the comparisons and justifications line up
+neatly:
+#+BEGIN_SRC lean
+theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l
+| []       := rfl
+| (a :: l) := calc
+    reverse (reverse (a :: l)) = reverse (concat a (reverse l))     : rfl
+                           ... = reverse (reverse l ++ [a])         : concat_eq_append
+                           ... = reverse [a] ++ reverse (reverse l) : reverse_append
+                           ... = reverse [a] ++ l                   : reverse_reverse
+                           ... = a :: l                             : rfl
+#+END_SRC lean
+To be more compact, for example, you may do this only after the first line:
+#+BEGIN_SRC lean
+theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l
+| []       := rfl
+| (a :: l) := calc
+    reverse (reverse (a :: l)) 
+          = reverse (concat a (reverse l))     : rfl
+      ... = reverse (reverse l ++ [a])         : concat_eq_append
+      ... = reverse [a] ++ reverse (reverse l) : reverse_append
+      ... = reverse [a] ++ l                   : reverse_reverse
+      ... = a :: l                             : rfl
+#+END_SRC lean
+
+Sections
+--------
+
+Within a section, you can indent definitions and theorems to make the
+scope salient:
+#+BEGIN_SRC lean
+section my_section
+  variable A : Type
+  variable P : Prop
+
+  definition foo (x : A) : A := x
+
+  theorem bar (H : P) : P := H
+end my_section
+#+END_SRC
+If the section is long, however, you can omit the indents.
+
+We generally use a blank line to separate theorems and definitions,
+but this can be omitted, for example, to group together a number of
+short definitions, or to group together a definition and notation.
+
+Comments
+--------
+
+Use comment delimeters =/-= =-/= to provide section headers and
+separators, and for long comments. Use =--= for short or in-line
+comments.