doc(data/list/*): Add missing documentation (#8867)

Fixing the missing module docstrings in `data/list`, as well as documenting some `def`s and `theorem`s.

src/data/list/alist.lean

@@ -6,7 +6,13 @@ Authors: Sean Leather, Mario Carneiro
 import data.list.sigma
 
 /-!
-# Association lists
+# Association Lists
+
+This file makes use of the contents of the `data.list.sigma` file to define association lists. These
+association lists are represented by the `alist` structure, which comprises a list of sigmas as a
+key-value store, as well as a proof that this has no duplicate keys.
+
+The file provides ways to access, modify, and combine `alist`s.
 -/
 
 universes u v w

src/data/list/func.lean

@@ -5,6 +5,25 @@ Authors: Seul Baek
 -/
 import data.nat.basic
 
+/-!
+# Lists as Functions
+
+Definitions for using lists as finite representations of finitely-supported functions with domain
+ℕ.
+
+These include pointwise operations on lists, as well as get and set operations.
+
+## Notations
+
+An index notation is introduced in this file for setting a particular element of a list. With `as`
+as a list `m` as an index, and `a` as a new element, the notation is `as {m ↦ a}`.
+
+So, for example
+`[1, 3, 5] {1 ↦ 9}` would result in `[1, 9, 5]`
+
+This notation is in the locale `list.func`.
+-/
+
 open list
 
 universes u v w
@@ -16,12 +35,15 @@ namespace func
 variables {a : α}
 variables {as as1 as2 as3 : list α}
 
-/- Definitions for using lists as finite
-   representations of functions with domain ℕ. -/
+/-- Elementwise negation of a list -/
 def neg [has_neg α] (as : list α) := as.map (λ a, -a)
 
 variables [inhabited α] [inhabited β]
 
+/--
+Update element of a list by index. If the index is out of range, extend the list with default
+elements
+-/
 @[simp] def set (a : α) : list α → ℕ → list α
 | (_::as) 0     := a::as
 | []      0     := [a]
@@ -30,23 +52,31 @@ variables [inhabited α] [inhabited β]
 
 localized "notation as ` {` m ` ↦ ` a `}` := list.func.set a as m" in list.func
 
+/-- Get element of a list by index. If the index is out of range, return the default element -/
 @[simp] def get : ℕ → list α → α
 | _ []          := default α
 | 0 (a::as)     := a
 | (n+1) (a::as) := get n as
 
+/--
+Pointwise equality of lists. If lists are different lengths, compare with the default
+element.
+-/
 def equiv (as1 as2 : list α) : Prop :=
 ∀ (m : nat), get m as1 = get m as2
 
+/-- Pointwise operations on lists. If lists are different lengths, use the default element. -/
 @[simp] def pointwise (f : α → β → γ) : list α → list β → list γ
 | []      []      := []
 | []      (b::bs) := map (f $ default α) (b::bs)
 | (a::as) []      := map (λ x, f x $ default β) (a::as)
 | (a::as) (b::bs) := (f a b)::(pointwise as bs)
 
+/-- Pointwise addition on lists. If lists are different lengths, use zero. -/
 def add {α : Type u} [has_zero α] [has_add α] : list α → list α → list α :=
 @pointwise α α α ⟨0⟩ ⟨0⟩ (+)
 
+/-- Pointwise subtraction on lists. If lists are different lengths, use zero. -/
 def sub {α : Type u} [has_zero α] [has_sub α] : list α → list α → list α :=
 @pointwise α α α ⟨0⟩ ⟨0⟩ (@has_sub.sub α _)
 

src/data/list/of_fn.lean

@@ -6,24 +6,38 @@ Authors: Mario Carneiro
 import data.list.basic
 import data.fin
 
+/-!
+# Lists from functions
+
+Theorems and lemmas for dealing with `list.of_fn`, which converts a function on `fin n` to a list
+of length n.
+
+## Main Definitions
+
+The main definitions pertain to lists generated using `of_fn`
+
+- `list.length_of_fn`, which tells us the length of such a list
+- `list.nth_of_fn`, which tells us the nth element of such a list
+- `list.array_eq_of_fn`, which interprets the list form of an array as such a list.
+-/
+
 universes u
 
 variables {α : Type u}
 
 open nat
 namespace list
 
-/- of_fn -/
-
-theorem length_of_fn_aux {n} (f : fin n → α) :
+lemma length_of_fn_aux {n} (f : fin n → α) :
   ∀ m h l, length (of_fn_aux f m h l) = length l + m
 | 0        h l := rfl
 | (succ m) h l := (length_of_fn_aux m _ _).trans (succ_add _ _)
 
+/-- The length of a list converted from a function is the size of the domain. -/
 @[simp] theorem length_of_fn {n} (f : fin n → α) : length (of_fn f) = n :=
 (length_of_fn_aux f _ _ _).trans (zero_add _)
 
-theorem nth_of_fn_aux {n} (f : fin n → α) (i) :
+lemma nth_of_fn_aux {n} (f : fin n → α) (i) :
   ∀ m h l,
     (∀ i, nth l i = of_fn_nth_val f (i + m)) →
      nth (of_fn_aux f m h l) i = of_fn_nth_val f i
@@ -34,6 +48,7 @@ theorem nth_of_fn_aux {n} (f : fin n → α) (i) :
   { simp only [nth, H, add_succ, succ_add] }
 end
 
+/-- The `n`th element of a list -/
 @[simp] theorem nth_of_fn {n} (f : fin n → α) (i) :
   nth (of_fn f) i = of_fn_nth_val f i :=
 nth_of_fn_aux f _ _ _ _ $ λ i,
@@ -52,6 +67,7 @@ nth_le_of_fn f ⟨i, ((length_of_fn f) ▸ h)⟩
   map g (of_fn f) = of_fn (g ∘ f) :=
 ext_le (by simp) (λ i h h', by simp)
 
+/-- Arrays converted to lists are the same as `of_fn` on the indexing function of the array. -/
 theorem array_eq_of_fn {n} (a : array n α) : a.to_list = of_fn a.read :=
 suffices ∀ {m h l}, d_array.rev_iterate_aux a
   (λ i, cons) m h l = of_fn_aux (d_array.read a) m h l, from this,
@@ -60,6 +76,7 @@ begin
   simp only [d_array.rev_iterate_aux, of_fn_aux, IH]
 end
 
+/-- `of_fn` on an empty domain is the empty list. -/
 @[simp] theorem of_fn_zero (f : fin 0 → α) : of_fn f = [] := rfl
 
 @[simp] theorem of_fn_succ {n} (f : fin (succ n) → α) :

src/data/list/perm.lean

@@ -9,7 +9,14 @@ import data.list.zip
 import logic.relation
 
 /-!
-# List permutations
+# List Permutations
+
+This file introduces the `list.perm` relation, which is true if two lists are permutations of one
+another.
+
+## Notation
+
+The notation `~` is used for permutation equivalence.
 -/
 
 open_locale nat

src/data/list/sigma.lean

@@ -9,6 +9,22 @@ import data.list.perm
 import data.list.range
 import data.sigma
 
+/-!
+# Utilities for lists of sigmas
+
+This file includes several ways of interacting with `list (sigma β)`, treated as a key-value store.
+
+## Main Definitions
+
+- `list.keys` extracts the list of keys.
+- `list.nodupkeys` determines if the store has duplicate keys.
+- `list.lookup`/`lookup_all` accesses the value(s) of a particular key.
+- `list.kreplace` modifies a value.
+- `list.kerase` removes a value.
+- `list.kinsert` inserts a value.
+- `list.kunion` computes the union of two stores.
+-/
+
 universes u v
 
 namespace list