lean2/doc/lean/library_style.org

#+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.