feat(data/list/*): Miscellaneous lemmas (#13577)

A few lemmas about `list.chain`, `list.pairwise`. Also rename `list.chain_of_pairwise` to `list.pairwise.chain` for dot notation.

Author: YaelDillies

src/data/list/basic.lean

@@ -57,6 +57,8 @@ cons_injective.eq_iff
 theorem exists_cons_of_ne_nil {l : list α} (h : l ≠ nil) : ∃ b L, l = b :: L :=
 by { induction l with c l',  contradiction,  use [c,l'], }
 
+lemma set_of_mem_cons (l : list α) (a : α) : {x | x ∈ a :: l} = insert a {x | x ∈ l} := rfl
+
 /-! ### mem -/
 
 theorem mem_singleton_self (a : α) : a ∈ [a] := mem_cons_self _ _

src/data/list/chain.lean

@@ -22,7 +22,7 @@ open nat
 
 namespace list
 
-variables {α : Type u} {β : Type v} {R : α → α → Prop}
+variables {α : Type u} {β : Type v} {R r : α → α → Prop} {l l₁ l₂ : list α} {a b : α}
 
 mk_iff_of_inductive_prop list.chain list.chain_iff
 
@@ -105,21 +105,31 @@ 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 :=
+protected lemma pairwise.chain (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},
   simp only [chain_cons, forall_mem_cons] at r,
   exact chain_cons.2 ⟨r.1, IH r'⟩
 end
 
+protected lemma chain.pairwise (tr : transitive R) :
+  ∀ {a : α} {l : list α}, chain R a l → pairwise R (a :: l)
+| a [] chain.nil := pairwise_singleton _ _
+| a _ (@chain.cons _ _ _ b l h hb) := hb.pairwise.cons begin
+    simp only [mem_cons_iff, forall_eq_or_imp, h, true_and],
+    exact λ c hc, tr h (rel_of_pairwise_cons hb.pairwise hc),
+  end
+
 theorem chain_iff_pairwise (tr : transitive R) {a : α} {l : list α} :
   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],
-  show ∀ x ∈ l, R b x, from λ x m, (tr r (rel_of_pairwise_cons IH m)),
-end, chain_of_pairwise⟩
+⟨chain.pairwise tr, pairwise.chain⟩
+
+protected lemma chain.sublist [is_trans α R] (hl : l₂.chain R a) (h : l₁ <+ l₂) : l₁.chain R a :=
+by { rw chain_iff_pairwise (transitive_of_trans R) at ⊢ hl, exact hl.sublist (h.cons_cons a) }
+
+protected lemma chain.rel [is_trans α R] (hl : l.chain R a) (hb : b ∈ l) : R a b :=
+by { rw chain_iff_pairwise (transitive_of_trans R) at hl, exact rel_of_pairwise_cons hl hb }
 
 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),
@@ -192,13 +202,16 @@ theorem chain'_map_of_chain' {S : β → β → Prop} (f : α → β)
 
 theorem pairwise.chain' : ∀ {l : list α}, pairwise R l → chain' R l
 | []       _ := trivial
-| (a :: l) h := chain_of_pairwise h
+| (a :: l) h := pairwise.chain 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
 
+protected lemma chain'.sublist [is_trans α R] (hl : l₂.chain' R) (h : l₁ <+ l₂) : l₁.chain' R :=
+by { rw chain'_iff_pairwise (transitive_of_trans R) at ⊢ hl, exact hl.sublist h }
+
 theorem chain'.cons {x y l} (h₁ : R x y) (h₂ : chain' R (y :: l)) :
   chain' R (x :: y :: l) :=
 chain'_cons.2 ⟨h₁, h₂⟩
@@ -289,7 +302,6 @@ lemma chain'.append_overlap : ∀ {l₁ l₂ l₃ : list α}
   exact ⟨h₁.1, chain'.append_overlap h₁.2 h₂ (cons_ne_nil _ _)⟩
 end
 
-variables {r : α → α → Prop} {a b : α}
 /--
 If `a` and `b` are related by the reflexive transitive closure of `r`, then there is a `r`-chain
 starting from `a` and ending on `b`.

src/data/list/cycle.lean

@@ -802,7 +802,7 @@ begin
   have Ha : a ∈ ((a :: l) : cycle α) := by simp,
   have Hl : ∀ {b} (hb : b ∈ l), b ∈ ((a :: l) : cycle α) := λ b hb, by simp [hb],
   rw cycle.chain_coe_cons,
-  apply chain_of_pairwise,
+  apply pairwise.chain,
   rw pairwise_cons,
   refine ⟨λ b hb, _, pairwise_append.2 ⟨pairwise_of_forall_mem_list
     (λ b hb c hc, hs b (Hl hb) c (Hl hc)), pairwise_singleton r a, λ b hb c hc, _⟩⟩,

src/data/list/pairwise.lean

@@ -104,16 +104,24 @@ protected lemma pairwise.sublist : Π {l₁ l₂ : list α}, l₁ <+ l₂ → pa
 | ._ ._ (sublist.cons2 l₁ l₂ a s) (pairwise.cons i h) :=
   (h.sublist s).cons (ball.imp_left s.subset i)
 
-lemma pairwise.forall_of_forall (H : symmetric R) (H₁ : ∀ x ∈ l, R x x) (H₂ : l.pairwise R) :
+lemma pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : l.pairwise R)
+  (h₃ : l.pairwise (flip R)) :
   ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y :=
 begin
-  induction l with a l IH, { exact forall_mem_nil _ },
-  cases forall_mem_cons.1 H₁ with H₁₁ H₁₂,
-  cases pairwise_cons.1 H₂ with H₂₁ H₂₂,
+  induction l with a l ih,
+  { exact forall_mem_nil _ },
+  rw pairwise_cons at h₂ h₃,
   rintro x (rfl | hx) y (rfl | hy),
-  exacts [H₁₁, H₂₁ _ hy, H (H₂₁ _ hx), IH H₁₂ H₂₂ hx hy]
+  { exact h₁ _ (l.mem_cons_self _) },
+  { exact h₂.1 _ hy },
+  { exact h₃.1 _ hx },
+  { exact ih (λ x hx, h₁ _ $ mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy }
 end
 
+lemma pairwise.forall_of_forall (H : symmetric R) (H₁ : ∀ x ∈ l, R x x) (H₂ : l.pairwise R) :
+  ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y :=
+H₂.forall_of_forall_of_flip H₁ $ by rwa H.flip_eq
+
 lemma pairwise.forall (hR : symmetric R) (hl : l.pairwise R) :
   ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b :=
 pairwise.forall_of_forall

src/logic/basic.lean

@@ -907,6 +907,21 @@ lemma congr_arg2 {α β γ : Sort*} (f : α → β → γ) {x x' : α} {y y' : 
   (hx : x = x') (hy : y = y') : f x y = f x' y' :=
 by { subst hx, subst hy }
 
+variables {β : α → Sort*} {γ : Π a, β a → Sort*} {δ : Π a b, γ a b → Sort*}
+
+lemma congr_fun₂ {f g : Π a b, γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b :=
+congr_fun (congr_fun h _) _
+
+lemma congr_fun₃ {f g : Π a b c, δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
+  f a b c = g a b c :=
+congr_fun₂ (congr_fun h _) _ _
+
+lemma funext₂ {f g : Π a, β a → Prop} (h : ∀ a b, f a b = g a b) : f = g :=
+funext $ λ _, funext $ h _
+
+lemma funext₃ {f g : Π a b, γ a b → Prop} (h : ∀ a b c, f a b c = g a b c) : f = g :=
+funext $ λ _, funext₂ $ h _
+
 end equality
 
 /-! ### Declarations about quantifiers -/

src/logic/relation.lean

@@ -71,6 +71,12 @@ is_refl.reflexive.ne_imp_iff
 
 protected lemma symmetric.iff (H : symmetric r) (x y : α) : r x y ↔ r y x := ⟨λ h, H h, λ h, H h⟩
 
+lemma symmetric.flip_eq (h : symmetric r) : flip r = r := funext₂ $ λ _ _, propext $ h.iff _ _
+lemma symmetric.swap_eq : symmetric r → swap r = r := symmetric.flip_eq
+
+lemma flip_eq_iff : flip r = r ↔ symmetric r := ⟨λ h x y, (congr_fun₂ h _ _).mp, symmetric.flip_eq⟩
+lemma swap_eq_iff : swap r = r ↔ symmetric r := flip_eq_iff
+
 end ne_imp
 
 section comap