doc(data/fin): add docs; fin_zero_elim -> fin.elim0; fin_zero_elim' -…

…> fin_zero_elim (#2055)

* doc(data/fin): add some docs

Also drom `fin_zero_elim` in favor of `fin.elim0` from `stdlib` and
rename `fin_zero_elim'` to `fin_zero_elim`.

* Update src/data/fin.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update docs, fix `Π` vs `∀`.

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/fin.lean

@@ -2,20 +2,66 @@
 Copyright (c) 2017 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek
-
-More about finite numbers.
 -/
 import data.nat.basic
+/-!
+# The finite type with `n` elements
+
+`fin n` is the type whose elements are natural numbers smaller than `n`.
+This file expands on the development in the core library.
+
+## Main definitions
+
+### Induction principles
+
+* `fin_zero.elim` : Elimination principle for the empty set `fin 0`, generalizes `fin.elim0`.
+* `fin.succ_rec` : Define `C n i` by induction on  `i : fin n` interpreted
+  as `(0 : fin (n - i)).succ.succ…`. This function has two arguments: `H0 n` defines
+  `0`-th element `C (n+1) 0` of an `(n+1)`-tuple, and `Hs n i` defines `(i+1)`-st element
+  of `(n+1)`-tuple based on `n`, `i`, and `i`-th element of `n`-tuple.
+* `fin.succ_rec_on` : same as `fin.succ_rec` but `i : fin n` is the first argument;
+
+### Casts
+
+* `cast_lt i h` : embed `i` into a `fin` where `h` proves it belongs into;
+* `cast_le h` : embed `fin n` into `fin m`, `h : n ≤ m`;
+* `cast eq` : embed `fin n` into `fin m`, `eq : n = m`;
+* `cast_add m` : embed `fin n` into `fin (n+m)`;
+* `cast_succ` : embed `fin n` into `fin (n+1)`;
+* `succ_above p` : embed `fin n` into `fin (n + 1)` with a hole around `p`;
+* `pred_above p i h` : embed `i : fin (n+1)` into `fin n` by ignoring `p`;
+* `sub_nat i h` : subtract `m` from `i ≥ m`, generalizes `fin.pred`;
+* `add_nat i h` : add `m` on `i` on the right, generalizes `fin.succ`;
+* `nat_add i h` adds `n` on `i` on the left;
+* `clamp n m` : `min n m` as an element of `fin (m + 1)`;
+
+### Operation on tuples
+
+We interpret maps `Π i : fin n, α i` as tuples `(α 0, …, α (n-1))`.
+If `α i` is a constant map, then tuples are isomorphic (but not definitionally equal)
+to `vector`s.
+
+We define the following operations:
+
+* `tail` : the tail of an `n+1` tuple, i.e., its last `n` entries;
+* `cons` : adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple;
+* `init` : the beginning of an `n+1` tuple, i.e., its first `n` entries;
+* `snoc` : adding an element at the end of an `n`-tuple, to get an `n+1`-tuple. The name `snoc` comes
+  from `cons` (i.e., adding an element to the left of a tuple) read in reverse order.
+* `find p` : returns the first index `n` where `p n` is satisfied, and `none` if it is never
+  satisfied.
+
+### Misc definitions
+
+* `fin.last n` : The greatest value of `fin (n+1)`.
+
+-/
 
 universe u
 open fin nat function
 
-/-- `fin 0` is empty -/
-def fin_zero_elim {C : Sort*} : fin 0 → C :=
-λ x, false.elim $ nat.not_lt_zero x.1 x.2
-
-def fin_zero_elim' {α : fin 0 → Sort u} : ∀(x : fin 0), α x
-| ⟨n, hn⟩ := false.elim (nat.not_lt_zero n hn)
+/-- Elimination principle for the empty set `fin 0`, dependent version. -/
+def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) : α x := x.elim0
 
 namespace fin
 variables {n m : ℕ} {a b : fin n}
@@ -180,6 +226,7 @@ lemma cast_succ_fin_succ (n : ℕ) (j : fin n) :
   cast_succ (fin.succ j) = fin.succ (cast_succ j) :=
 by simp [fin.ext_iff]
 
+/-- `min n m` as an element of `fin (m + 1)` -/
 def clamp (n m : ℕ) : fin (m + 1) := fin.of_nat $ min n m
 
 @[simp] lemma clamp_val (n m : ℕ) : (clamp n m).val = min n m :=
@@ -228,18 +275,28 @@ end
 
 section rec
 
+/-- Define `C n i` by induction on  `i : fin n` interpreted as `(0 : fin (n - i)).succ.succ…`.
+This function has two arguments: `H0 n` defines `0`-th element `C (n+1) 0` of an `(n+1)`-tuple,
+and `Hs n i` defines `(i+1)`-st element of `(n+1)`-tuple based on `n`, `i`, and `i`-th element
+of `n`-tuple. -/
 @[elab_as_eliminator] def succ_rec
-  {C : ∀ n, fin n → Sort*}
-  (H0 : ∀ n, C (succ n) 0)
-  (Hs : ∀ n i, C n i → C (succ n) i.succ) : ∀ {n : ℕ} (i : fin n), C n i
+  {C : Π n, fin n → Sort*}
+  (H0 : Π n, C (succ n) 0)
+  (Hs : Π n i, C n i → C (succ n) i.succ) : Π {n : ℕ} (i : fin n), C n i
 | 0        i           := i.elim0
 | (succ n) ⟨0, _⟩      := H0 _
 | (succ n) ⟨succ i, h⟩ := Hs _ _ (succ_rec ⟨i, lt_of_succ_lt_succ h⟩)
 
+/-- Define `C n i` by induction on  `i : fin n` interpreted as `(0 : fin (n - i)).succ.succ…`.
+This function has two arguments: `H0 n` defines `0`-th element `C (n+1) 0` of an `(n+1)`-tuple,
+and `Hs n i` defines `(i+1)`-st element of `(n+1)`-tuple based on `n`, `i`, and `i`-th element
+of `n`-tuple.
+
+A version of `fin.succ_rec` taking `i : fin n` as the first argument. -/
 @[elab_as_eliminator] def succ_rec_on {n : ℕ} (i : fin n)
-  {C : ∀ n, fin n → Sort*}
-  (H0 : ∀ n, C (succ n) 0)
-  (Hs : ∀ n i, C n i → C (succ n) i.succ) : C n i :=
+  {C : Π n, fin n → Sort*}
+  (H0 : Π n, C (succ n) 0)
+  (Hs : Π n i, C n i → C (succ n) i.succ) : C n i :=
 i.succ_rec H0 Hs
 
 @[simp] theorem succ_rec_on_zero {C : ∀ n, fin n → Sort*} {H0 Hs} (n) :
@@ -250,9 +307,11 @@ rfl
   @fin.succ_rec_on (succ n) i.succ C H0 Hs = Hs n i (fin.succ_rec_on i H0 Hs) :=
 by cases i; refl
 
+/-- Define `f : Π i : fin n.succ, C i` by separately handling the cases `i = 0` and
+`i = j.succ`, `j : fin n`. -/
 @[elab_as_eliminator] def cases
-  {C : fin (succ n) → Sort*} (H0 : C 0) (Hs : ∀ i : fin n, C (i.succ)) :
-  ∀ (i : fin (succ n)), C i
+  {C : fin (succ n) → Sort*} (H0 : C 0) (Hs : Π i : fin n, C (i.succ)) :
+  Π (i : fin (succ n)), C i
 | ⟨0, h⟩ := H0
 | ⟨succ i, h⟩ := Hs ⟨i, lt_of_succ_lt_succ h⟩
 
@@ -285,7 +344,7 @@ operations, first about adding or removing elements at the beginning of a tuple.
 
 /-- There is exactly one tuple of size zero. -/
 instance tuple0_unique (α : fin 0 → Type u) : unique (Π i : fin 0, α i) :=
-{ default := fin_zero_elim', uniq := λ x, funext fin_zero_elim' }
+{ default := fin_zero_elim, uniq := λ x, funext fin_zero_elim }
 
 variables {α : fin (n+1) → Type u} (x : α 0) (q : Πi, α i) (p : Π(i : fin n), α (i.succ))
 (i : fin n) (y : α i.succ) (z : α 0)