feat(Combinatorics/SimpleGraph): the reverse of a cycle is a cycle (#19611)

Added the result that a reverse cycle is a cycle. 
Includes supporting lemmas concerning lists. In preparation for Tutte's theorem.



Co-authored-by: Pim Otte <otte.pim@gmail.com>

Author: pimotte

Mathlib/Combinatorics/SimpleGraph/Path.lean

@@ -249,6 +249,15 @@ theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
   have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
   tauto
 
+protected lemma IsCycle.reverse {p : G.Walk u u} (h : p.IsCycle) : p.reverse.IsCycle := by
+  simp only [Walk.isCycle_def, nodup_tail_support_reverse] at h ⊢
+  exact ⟨h.1.reverse, fun h' ↦ h.2.1 (by simp_all [← Walk.length_eq_zero_iff]), h.2.2⟩
+
+@[simp]
+lemma isCycle_reverse {p : G.Walk u u} : p.reverse.IsCycle ↔ p.IsCycle where
+  mp h := by simpa using h.reverse
+  mpr := .reverse
+
 lemma IsPath.tail {p : G.Walk u v} (hp : p.IsPath) (hp' : ¬ p.Nil) : p.tail.IsPath := by
   rw [Walk.isPath_def] at hp ⊢
   rw [← cons_support_tail _ hp', List.nodup_cons] at hp

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -557,6 +557,20 @@ theorem subset_support_append_right {V : Type u} {G : SimpleGraph V} {u v w : V}
   intro h
   simp +contextual only [mem_support_append_iff, or_true, imp_true_iff]
 
+lemma getVert_eq_support_get? {u v n} (p : G.Walk u v) (h2 : n ≤ p.length) :
+    p.getVert n = p.support[n]? := by
+  match p with
+  | .nil => simp_all
+  | .cons h q =>
+    simp only [Walk.support_cons]
+    by_cases hn : n = 0
+    · simp only [hn, getVert_zero, List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem,
+      List.getElem_cons_zero]
+    · push_neg at hn
+      nth_rewrite 2 [show n = (n - 1) + 1 from by omega]
+      rw [Walk.getVert_cons q h hn, List.getElem?_cons_succ]
+      exact getVert_eq_support_get? q (Nat.sub_le_of_le_add (Walk.length_cons _ _ ▸ h2))
+
 theorem coe_support {u v : V} (p : G.Walk u v) :
     (p.support : Multiset V) = {u} + p.support.tail := by cases p <;> rfl
 
@@ -739,6 +753,14 @@ theorem edges_nodup_of_support_nodup {u v : V} {p : G.Walk u v} (h : p.support.N
     simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
     exact ⟨fun h' => h.1 (fst_mem_support_of_mem_edges p' h'), ih h.2⟩
 
+theorem nodup_tail_support_reverse {u : V} {p : G.Walk u u} :
+    p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup := by
+  rw [Walk.support_reverse]
+  refine List.nodup_tail_reverse p.support ?h
+  rw [← getVert_eq_support_get? _ (by omega), List.getLast?_eq_getElem?,
+    ← getVert_eq_support_get? _ (by rw [Walk.length_support]; omega)]
+  aesop
+
 theorem edges_injective {u v : V} : Function.Injective (Walk.edges : G.Walk u v → List (Sym2 V))
   | .nil, .nil, _ => rfl
   | .nil, .cons _ _, h => by simp at h

Mathlib/Data/List/Basic.lean

@@ -1032,6 +1032,15 @@ theorem cons_get_drop_succ {l : List α} {n} :
     l.get n :: l.drop (n.1 + 1) = l.drop n.1 :=
   (drop_eq_getElem_cons n.2).symm
 
+lemma drop_length_sub_one {l : List α} (h : l ≠ []) : l.drop (l.length - 1) = [l.getLast h] := by
+  induction l with
+  | nil => aesop
+  | cons a l ih =>
+    by_cases hl : l = []
+    · aesop
+    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
+    aesop
+
 section TakeI
 
 variable [Inhabited α]

Mathlib/Data/List/Nodup.lean

@@ -227,6 +227,21 @@ theorem Nodup.filter (p : α → Bool) {l} : Nodup l → Nodup (filter p l) := b
 theorem nodup_reverse {l : List α} : Nodup (reverse l) ↔ Nodup l :=
   pairwise_reverse.trans <| by simp only [Nodup, Ne, eq_comm]
 
+lemma nodup_tail_reverse (l : List α) (h : l[0]? = l.getLast?) :
+    Nodup l.reverse.tail ↔ Nodup l.tail := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    by_cases hl : l = []
+    · aesop
+    · simp_all only [List.get?_eq_getElem?, List.tail_reverse, List.nodup_reverse,
+        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
+      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem, getElem_cons_zero,
+        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
+        show l.length ≠ 0 from by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
+      rw [h, show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup from by
+        simp [List.dropLast_eq_take, ← List.drop_length_sub_one], List.nodup_append_comm]
+      simp [List.getLast_eq_getElem]
 
 theorem Nodup.erase_getElem [DecidableEq α] {l : List α} (hl : l.Nodup)
     (i : Nat) (h : i < l.length) : l.erase l[i] = l.eraseIdx ↑i := by