lean2/doc/lean/library_style.org

332 lines
10 KiB
Org Mode
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

#+Title: Library Style Guidelines
#+Author: [[http://www.andrew.cmu.edu/user/avigad][Jeremy Avigad]]
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 @algebra.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 nat.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_ge
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
open nat
theorem two_step_induction_on {P : nat → Prop} (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
open nat
theorem two_step_induction_on {P : nat → Prop} (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
open nat
theorem nat_case {P : nat → Prop} (n : nat) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
nat.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
open nat
axiom zero_or_succ (n : nat) : n = zero n = succ (pred n)
theorem nat_discriminate {B : Prop} {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
import data.list
open list eq.ops
variable {T : Type}
local attribute mem [reducible]
local attribute append [reducible]
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
open nat
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
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
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
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
import data.nat
open nat eq
theorem add_right_inj {n m k : nat} : n + m = n + k → m = k :=
nat.induction_on n
(take H : 0 + m = 0 + k,
calc
m = 0 + m : symm (zero_add m)
... = 0 + k : H
... = k : zero_add)
(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 (succ_add n m)
... = succ n + k : H
... = succ (n + k) : succ_add 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 :=
take (X : Type) (x : X), exists.intro x rfl
#+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
import data.list
open list
variable {T : Type}
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
To be more compact, for example, you may do this only after the first line:
#+BEGIN_SRC lean
import data.list
open list
variable {T : Type}
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.