From a7faaf53e05ca2a80a2afc3888d7d823fd1440c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 25 Jun 2021 18:48:53 +0000
Subject: [PATCH] docs(data/list/chain): add module docstring (#8041)

---
 src/data/list/chain.lean | 108 +++++++++++++++++++++------------------
 1 file changed, 57 insertions(+), 51 deletions(-)

diff --git a/src/data/list/chain.lean b/src/data/list/chain.lean
index 4432e690c0afd..6c32f98a89be0 100644
--- a/src/data/list/chain.lean
+++ b/src/data/list/chain.lean
@@ -6,26 +6,32 @@ Authors: Mario Carneiro, Kenny Lau, Yury Kudryashov
 import data.list.pairwise
 import logic.relation
 
+/-!
+# Relation chain
+
+This file provides basic results about `list.chain` (definition in `data.list.defs`).
+A list `[a₂, ..., aₙ]` is a `chain` starting at `a₁` with respect to the relation `r` if `r a₁ a₂`
+and `r a₂ a₃` and ... and `r aₙ₋₁ aₙ`. We write it `chain r a₁ [a₂, ..., aₙ]`.
+A graph-specialized version is in development and will hopefully be added under `combinatorics.`
+sometime soon.
+-/
+
 universes u v
 
 open nat
 
-variables {α : Type u} {β : Type v}
-
 namespace list
 
-/- chain relation (conjunction of R a b ∧ R b c ∧ R c d ...) -/
+variables {α : Type u} {β : Type v} {R : α → α → Prop}
 
 mk_iff_of_inductive_prop list.chain list.chain_iff
 
-variable {R : α → α → Prop}
-
 theorem rel_of_chain_cons {a b : α} {l : list α}
-  (p : chain R a (b::l)) : R a b :=
+  (p : chain R a (b :: l)) : R a b :=
 (chain_cons.1 p).1
 
 theorem chain_of_chain_cons {a b : α} {l : list α}
-  (p : chain R a (b::l)) : chain R b l :=
+  (p : chain R a (b :: l)) : chain R b l :=
 (chain_cons.1 p).2
 
 theorem chain.imp' {S : α → α → Prop}
@@ -53,8 +59,8 @@ theorem chain.iff_mem {a : α} {l : list α} :
 theorem chain_singleton {a b : α} : chain R a [b] ↔ R a b :=
 by simp only [chain_cons, chain.nil, and_true]
 
-theorem chain_split {a b : α} {l₁ l₂ : list α} : chain R a (l₁++b::l₂) ↔
-  chain R a (l₁++[b]) ∧ chain R b l₂ :=
+theorem chain_split {a b : α} {l₁ l₂ : list α} : chain R a (l₁ ++ b :: l₂) ↔
+  chain R a (l₁ ++ [b]) ∧ chain R b l₂ :=
 by induction l₁ with x l₁ IH generalizing a;
 simp only [*, nil_append, cons_append, chain.nil, chain_cons, and_true, and_assoc]
 
@@ -95,7 +101,7 @@ begin
   { simp [H _ _ _ _ (rel_of_chain_cons hl₂), l_ih _ _ (chain_of_chain_cons hl₂)] }
 end
 
-theorem chain_of_pairwise {a : α} {l : list α} (p : pairwise R (a::l)) : chain R a l :=
+theorem chain_of_pairwise {a : α} {l : list α} (p : pairwise R (a :: l)) : chain R a l :=
 begin
   cases pairwise_cons.1 p with r p', clear p,
   induction p' with b l r' p IH generalizing a, {exact chain.nil},
@@ -104,7 +110,7 @@ begin
 end
 
 theorem chain_iff_pairwise (tr : transitive R) {a : α} {l : list α} :
-  chain R a l ↔ pairwise R (a::l) :=
+  chain R a l ↔ pairwise R (a :: l) :=
 ⟨λ c, begin
   induction c with b b c l r p IH, {exact pairwise_singleton _ _},
   apply IH.cons _, simp only [mem_cons_iff, forall_eq_or_imp, r, true_and],
@@ -114,26 +120,26 @@ end, chain_of_pairwise⟩
 theorem chain_iff_nth_le {R} : ∀ {a : α} {l : list α},
   chain R a l ↔ (∀ h : 0 < length l, R a (nth_le l 0 h)) ∧ (∀ i (h : i < length l - 1),
     R (nth_le l i (lt_of_lt_pred h)) (nth_le l (i+1) (lt_pred_iff.mp h)))
-| a [] := by simp
+| a []       := by simp
 | a (b :: t) :=
 begin
   rw [chain_cons, chain_iff_nth_le],
   split,
-  { rintros ⟨R, ⟨h0, h⟩⟩,
+  { rintro ⟨R, ⟨h0, h⟩⟩,
     split,
-    { intro w, exact R, },
-    { intros i w,
-      cases i,
-      { apply h0, },
-      { convert h i _ using 1,
-        simp only [succ_eq_add_one, add_succ_sub_one, add_zero, length, add_lt_add_iff_right] at w,
-        exact lt_pred_iff.mpr w, } } },
-  { rintros ⟨h0, h⟩, split,
-    { apply h0, simp, },
-    { split,
-      { apply h 0, },
-      { intros i w, convert h (i+1) _ using 1,
-        exact lt_pred_iff.mp w, } } },
+    { intro w, exact R },
+    intros i w,
+    cases i,
+    { apply h0 },
+    convert h i _ using 1,
+    simp only [succ_eq_add_one, add_succ_sub_one, add_zero, length, add_lt_add_iff_right] at w,
+    exact lt_pred_iff.mpr w, },
+  rintro ⟨h0, h⟩, split,
+  { apply h0, simp, },
+  split,
+  { apply h 0, },
+  intros i w, convert h (i+1) _ using 1,
+  exact lt_pred_iff.mp w,
 end
 
 theorem chain'.imp {S : α → α → Prop}
@@ -145,8 +151,8 @@ theorem chain'.iff {S : α → α → Prop}
 ⟨chain'.imp (λ a b, (H a b).1), chain'.imp (λ a b, (H a b).2)⟩
 
 theorem chain'.iff_mem : ∀ {l : list α}, chain' R l ↔ chain' (λ x y, x ∈ l ∧ y ∈ l ∧ R x y) l
-| [] := iff.rfl
-| (x::l) :=
+| []       := iff.rfl
+| (x :: l) :=
   ⟨λ h, (chain.iff_mem.1 h).imp $ λ a b ⟨h₁, h₂, h₃⟩, ⟨h₁, or.inr h₂, h₃⟩,
    chain'.imp $ λ a b h, h.2.2⟩
 
@@ -154,10 +160,10 @@ theorem chain'.iff_mem : ∀ {l : list α}, chain' R l ↔ chain' (λ x y, x ∈
 
 @[simp] theorem chain'_singleton (a : α) : chain' R [a] := chain.nil
 
-theorem chain'_split {a : α} : ∀ {l₁ l₂ : list α}, chain' R (l₁++a::l₂) ↔
-  chain' R (l₁++[a]) ∧ chain' R (a::l₂)
-| []      l₂ := (and_iff_right (chain'_singleton a)).symm
-| (b::l₁) l₂ := chain_split
+theorem chain'_split {a : α} : ∀ {l₁ l₂ : list α}, chain' R (l₁ ++ a :: l₂) ↔
+  chain' R (l₁ ++ [a]) ∧ chain' R (a :: l₂)
+| []        l₂ := (and_iff_right (chain'_singleton a)).symm
+| (b :: l₁) l₂ := chain_split
 
 theorem chain'_map (f : β → α) {l : list β} :
   chain' R (map f l) ↔ chain' (λ a b : β, R (f a) (f b)) l :=
@@ -174,13 +180,13 @@ theorem chain'_map_of_chain' {S : β → β → Prop} (f : α → β)
 (chain'_map f).2 $ p.imp H
 
 theorem pairwise.chain' : ∀ {l : list α}, pairwise R l → chain' R l
-| [] _ := trivial
-| (a::l) h := chain_of_pairwise h
+| []       _ := trivial
+| (a :: l) h := chain_of_pairwise h
 
 theorem chain'_iff_pairwise (tr : transitive R) : ∀ {l : list α},
   chain' R l ↔ pairwise R l
-| [] := (iff_true_intro pairwise.nil).symm
-| (a::l) := chain_iff_pairwise tr
+| []       := (iff_true_intro pairwise.nil).symm
+| (a :: l) := chain_iff_pairwise tr
 
 @[simp] theorem chain'_cons {x y l} : chain' R (x :: y :: l) ↔ R x y ∧ chain' R (y :: l) :=
 chain_cons
@@ -202,7 +208,7 @@ by { rw ← cons_head'_tail hy at h, exact h.rel_head }
 
 theorem chain'.cons' {x} :
   ∀ {l : list α},  chain' R l → (∀ y ∈ l.head', R x y) → chain' R (x :: l)
-| [] _ _ := chain'_singleton x
+| []       _  _ := chain'_singleton x
 | (a :: l) hl H := hl.cons $ H _ rfl
 
 theorem chain'_cons' {x l} : chain' R (x :: l) ↔ (∀ y ∈ head' l, R x y) ∧ chain' R l :=
@@ -211,12 +217,12 @@ theorem chain'_cons' {x l} : chain' R (x :: l) ↔ (∀ y ∈ head' l, R x y) 
 theorem chain'.append : ∀ {l₁ l₂ : list α} (h₁ : chain' R l₁) (h₂ : chain' R l₂)
   (h : ∀ (x ∈ l₁.last') (y ∈ l₂.head'), R x y),
   chain' R (l₁ ++ l₂)
-| [] l₂ h₁ h₂ h := h₂
-| [a] l₂ h₁ h₂ h := h₂.cons' $ h _ rfl
-| (a::b::l) l₂ h₁ h₂ h :=
+| []            l₂ h₁ h₂ h := h₂
+| [a]           l₂ h₁ h₂ h := h₂.cons' $ h _ rfl
+| (a :: b :: l) l₂ h₁ h₂ h :=
   begin
     simp only [last'] at h,
-    have : chain' R (b::l) := h₁.tail,
+    have : chain' R (b :: l) := h₁.tail,
     exact (this.append h₂ h).cons h₁.rel_head
   end
 
@@ -228,28 +234,28 @@ theorem chain'.imp_head {x y} (h : ∀ {z}, R x z → R y z) {l} (hl : chain' R
 hl.tail.cons' $ λ z hz, h $ hl.rel_head' hz
 
 theorem chain'_reverse : ∀ {l}, chain' R (reverse l) ↔ chain' (flip R) l
-| [] := iff.rfl
-| [a] := by simp only [chain'_singleton, reverse_singleton]
+| []            := iff.rfl
+| [a]           := by simp only [chain'_singleton, reverse_singleton]
 | (a :: b :: l) := by rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append,
     nil_append, chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip]
 
 theorem chain'_iff_nth_le {R} : ∀ {l : list α},
   chain' R l ↔ ∀ i (h : i < length l - 1),
     R (nth_le l i (lt_of_lt_pred h)) (nth_le l (i+1) (lt_pred_iff.mp h))
-| [] := by simp
-| (a :: nil) := by simp
+| []            := by simp
+| [a]           := by simp
 | (a :: b :: t) :=
 begin
   rw [chain'_cons, chain'_iff_nth_le],
   split,
-  { rintros ⟨R, h⟩ i w,
+  { rintro ⟨R, h⟩ i w,
     cases i,
     { exact R, },
     { convert h i _ using 1,
       simp only [succ_eq_add_one, add_succ_sub_one, add_zero, length, add_lt_add_iff_right] at w,
       simpa using w, },
    },
-  { rintros h, split,
+  { rintro h, split,
     { apply h 0, simp, },
     { intros i w, convert h (i+1) _ using 1,
       simp only [add_zero, length, add_succ_sub_one] at w,
@@ -262,10 +268,10 @@ end
 lemma chain'.append_overlap : ∀ {l₁ l₂ l₃ : list α}
   (h₁ : chain' R (l₁ ++ l₂)) (h₂ : chain' R (l₂ ++ l₃)) (hn : l₂ ≠ []),
   chain' R (l₁ ++ l₂ ++ l₃)
-| [] l₂ l₃ h₁ h₂ hn := h₂
-| l₁ [] l₃ h₁ h₂ hn := (hn rfl).elim
-| [a] (b::l₂) l₃ h₁ h₂ hn := by { simp at *, tauto }
-| (a::b::l₁) (c::l₂) l₃ h₁ h₂ hn := begin
+| []             l₂        l₃ h₁ h₂ hn := h₂
+| l₁             []        l₃ h₁ h₂ hn := (hn rfl).elim
+| [a]            (b :: l₂) l₃ h₁ h₂ hn := by { simp at *, tauto }
+| (a :: b :: l₁) (c :: l₂) l₃ h₁ h₂ hn := begin
   simp only [cons_append, chain'_cons] at h₁ h₂ ⊢,
   simp only [← cons_append] at h₁ h₂ ⊢,
   exact ⟨h₁.1, chain'.append_overlap h₁.2 h₂ (cons_ne_nil _ _)⟩