feat(combinatorics/simple_graph/connectivity): concat and concat_rec (#17209)

Adds the alternative constructor for walks along with its recursion principle. (Borrowed from lean2/hott.)

Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: kmill

src/combinatorics/simple_graph/connectivity.lean

@@ -151,6 +151,13 @@ def append : Π {u v w : V}, G.walk u v → G.walk v w → G.walk u w
 | _ _ _ nil q := q
 | _ _ _ (cons h p) q := cons h (p.append q)
 
+/-- The reversed version of `simple_graph.walk.cons`, concatenating an edge to
+the end of a walk. -/
+def concat {u v w : V} (p : G.walk u v) (h : G.adj v w) : G.walk u w := p.append (cons h nil)
+
+lemma concat_eq_append {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  p.concat h = p.append (cons h nil) := rfl
+
 /-- The concatenation of the reverse of the first walk with the second walk. -/
 protected def reverse_aux : Π {u v w : V}, G.walk u v → G.walk u w → G.walk v w
 | _ _ _ nil q := q
@@ -215,6 +222,35 @@ lemma append_assoc : Π {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.w
   (hu : u = u') (hv : v = v') (hw : w = w') :
   (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw := by { subst_vars, refl }
 
+lemma concat_nil {u v : V} (h : G.adj u v) : nil.concat h = cons h nil := rfl
+
+@[simp] lemma concat_cons {u v w x : V} (h : G.adj u v) (p : G.walk v w) (h' : G.adj w x) :
+  (cons h p).concat h' = cons h (p.concat h') := rfl
+
+lemma append_concat {u v w x : V} (p : G.walk u v) (q : G.walk v w) (h : G.adj w x) :
+  p.append (q.concat h) = (p.append q).concat h := append_assoc _ _ _
+
+lemma concat_append {u v w x : V} (p : G.walk u v) (h : G.adj v w) (q : G.walk w x) :
+  (p.concat h).append q = p.append (cons h q) :=
+by rw [concat_eq_append, ← append_assoc, cons_nil_append]
+
+/-- A non-trivial `cons` walk is representable as a `concat` walk. -/
+lemma exists_cons_eq_concat : Π {u v w : V} (h : G.adj u v) (p : G.walk v w),
+  ∃ (x : V) (q : G.walk u x) (h' : G.adj x w), cons h p = q.concat h'
+| _ _ _ h nil := ⟨_, nil, h, rfl⟩
+| _ _ _ h (cons h' p) :=
+  begin
+    obtain ⟨y, q, h'', hc⟩ := exists_cons_eq_concat h' p,
+    refine ⟨y, cons h q, h'', _⟩,
+    rw [concat_cons, hc],
+  end
+
+/-- A non-trivial `concat` walk is representable as a `cons` walk. -/
+lemma exists_concat_eq_cons : Π {u v w : V} (p : G.walk u v) (h : G.adj v w),
+  ∃ (x : V) (h' : G.adj u x) (q : G.walk x w), p.concat h = cons h' q
+| _ _ _ nil h := ⟨_, h, nil, rfl⟩
+| _ _ _ (cons h' p) h := ⟨_, h', walk.concat p h, concat_cons _ _ _⟩
+
 @[simp] lemma reverse_nil {u : V} : (nil : G.walk u u).reverse = nil := rfl
 
 lemma reverse_singleton {u v : V} (h : G.adj u v) :
@@ -250,6 +286,10 @@ by simp [reverse]
   (p.append q).reverse = q.reverse.append p.reverse :=
 by simp [reverse]
 
+@[simp] lemma reverse_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  (p.concat h).reverse = cons (G.symm h) p.reverse :=
+by simp [concat_eq_append]
+
 @[simp] lemma reverse_reverse : Π {u v : V} (p : G.walk u v), p.reverse.reverse = p
 | _ _ nil := rfl
 | _ _ (cons h p) := by simp [reverse_reverse]
@@ -268,6 +308,9 @@ by { subst_vars, refl }
 | _ _ _ nil _ := by simp
 | _ _ _ (cons _ _) _ := by simp [length_append, add_left_comm, add_comm]
 
+@[simp] lemma length_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  (p.concat h).length = p.length + 1 := length_append _ _
+
 @[simp] protected lemma length_reverse_aux : Π {u v w : V} (p : G.walk u v) (q : G.walk u w),
   (p.reverse_aux q).length = p.length + q.length
 | _ _ _ nil _ := by simp!
@@ -291,6 +334,76 @@ end
 @[simp] lemma length_eq_zero_iff {u : V} {p : G.walk u u} : p.length = 0 ↔ p = nil :=
 by cases p; simp
 
+section concat_rec
+
+variables
+  {motive : Π (u v : V), G.walk u v → Sort*}
+  (Hnil : Π {u : V}, motive u u nil)
+  (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p → motive u w (p.concat h))
+
+/-- Auxiliary definition for `simple_graph.walk.concat_rec` -/
+def concat_rec_aux : Π {u v : V} (p : G.walk u v), motive v u p.reverse
+| _ _ nil := Hnil
+| _ _ (cons h p) := eq.rec (Hconcat p.reverse (G.symm h) (concat_rec_aux p)) (reverse_cons h p).symm
+
+/-- Recursor on walks by inducting on `simple_graph.walk.concat`.
+
+This is inducting from the opposite end of the walk compared
+to `simple_graph.walk.rec`, which inducts on `simple_graph.walk.cons`. -/
+@[elab_as_eliminator]
+def concat_rec {u v : V} (p : G.walk u v) : motive u v p :=
+eq.rec (concat_rec_aux @Hnil @Hconcat p.reverse) (reverse_reverse p)
+
+@[simp] lemma concat_rec_nil (u : V) :
+  @concat_rec _ _ motive @Hnil @Hconcat _ _ (nil : G.walk u u) = Hnil := rfl
+
+@[simp] lemma concat_rec_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  @concat_rec _ _ motive @Hnil @Hconcat _ _ (p.concat h)
+  = Hconcat p h (concat_rec @Hnil @Hconcat p) :=
+begin
+  simp only [concat_rec],
+  apply eq_of_heq,
+  apply rec_heq_of_heq,
+  transitivity concat_rec_aux @Hnil @Hconcat (cons h.symm p.reverse),
+  { congr, simp },
+  { rw [concat_rec_aux, rec_heq_iff_heq],
+    congr; simp [heq_rec_iff_heq], }
+end
+
+end concat_rec
+
+lemma concat_ne_nil {u v : V} (p : G.walk u v) (h : G.adj v u) :
+  p.concat h ≠ nil :=
+by cases p; simp [concat]
+
+lemma concat_inj {u v v' w : V}
+  {p : G.walk u v} {h : G.adj v w} {p' : G.walk u v'} {h' : G.adj v' w}
+  (he : p.concat h = p'.concat h') :
+  ∃ (hv : v = v'), p.copy rfl hv = p' :=
+begin
+  induction p,
+  { cases p',
+    { exact ⟨rfl, rfl⟩ },
+    { exfalso,
+      simp only [concat_nil, concat_cons] at he,
+      obtain ⟨rfl, he⟩ := he,
+      simp only [heq_iff_eq] at he,
+      exact concat_ne_nil _ _ he.symm, } },
+  { rw concat_cons at he,
+    cases p',
+    { exfalso,
+      simp only [concat_nil] at he,
+      obtain ⟨rfl, he⟩ := he,
+      rw [heq_iff_eq] at he,
+      exact concat_ne_nil _ _ he, },
+    { rw concat_cons at he,
+      simp only at he,
+      obtain ⟨rfl, he⟩ := he,
+      rw [heq_iff_eq] at he,
+      obtain ⟨rfl, rfl⟩ := p_ih he,
+      exact ⟨rfl, rfl⟩, } }
+end
+
 /-- The `support` of a walk is the list of vertices it visits in order. -/
 def support : Π {u v : V}, G.walk u v → list V
 | u v nil := [u]
@@ -310,6 +423,9 @@ def edges {u v : V} (p : G.walk u v) : list (sym2 V) := p.darts.map dart.edge
 @[simp] lemma support_cons {u v w : V} (h : G.adj u v) (p : G.walk v w) :
   (cons h p).support = u :: p.support := rfl
 
+@[simp] lemma support_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  (p.concat h).support = p.support.concat w := by induction p; simp [*, concat_nil]
+
 @[simp] lemma support_copy {u v u' v'} (p : G.walk u v) (hu : u = u') (hv : v = v') :
   (p.copy hu hv).support = p.support := by { subst_vars, refl }
 
@@ -427,6 +543,9 @@ edges_subset_edge_set p h
 @[simp] lemma darts_cons {u v w : V} (h : G.adj u v) (p : G.walk v w) :
   (cons h p).darts = ⟨(u, v), h⟩ :: p.darts := rfl
 
+@[simp] lemma darts_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  (p.concat h).darts = p.darts.concat ⟨(v, w), h⟩ := by induction p; simp [*, concat_nil]
+
 @[simp] lemma darts_copy {u v u' v'} (p : G.walk u v) (hu : u = u') (hv : v = v') :
   (p.copy hu hv).darts = p.darts := by { subst_vars, refl }
 
@@ -463,6 +582,9 @@ by simpa! using congr_arg list.init (map_fst_darts_append p)
 @[simp] lemma edges_cons {u v w : V} (h : G.adj u v) (p : G.walk v w) :
   (cons h p).edges = ⟦(u, v)⟧ :: p.edges := rfl
 
+@[simp] lemma edges_concat {u v w : V} (p : G.walk u v) (h : G.adj v w) :
+  (p.concat h).edges = p.edges.concat ⟦(v, w)⟧ := by simp [edges]
+
 @[simp] lemma edges_copy {u v u' v'} (p : G.walk u v) (hu : u = u') (hv : v = v') :
   (p.copy hu hv).edges = p.edges := by { subst_vars, refl }
 

src/logic/basic.lean

@@ -908,9 +908,17 @@ lemma heq_of_cast_eq :
 lemma cast_eq_iff_heq {α β : Sort*} {a : α} {a' : β} {e : α = β} : cast e a = a' ↔ a == a' :=
 ⟨heq_of_cast_eq _, λ h, by cases h; refl⟩
 
-lemma rec_heq_of_heq {β} {C : α → Sort*} {x : C a} {y : β} (eq : a = b) (h : x == y) :
-  @eq.rec α a C x b eq == y :=
-by subst eq; exact h
+lemma rec_heq_of_heq {β} {C : α → Sort*} {x : C a} {y : β} (e : a = b) (h : x == y) :
+  @eq.rec α a C x b e == y :=
+by subst e; exact h
+
+lemma rec_heq_iff_heq {β} {C : α → Sort*} {x : C a} {y : β} {e : a = b} :
+  @eq.rec α a C x b e == y ↔ x == y :=
+by subst e
+
+lemma heq_rec_iff_heq {β} {C : α → Sort*} {x : β} {y : C a} {e : a = b} :
+  x == @eq.rec α a C y b e ↔ x == y :=
+by subst e
 
 protected lemma eq.congr {x₁ x₂ y₁ y₂ : α} (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) :
   (x₁ = x₂) ↔ (y₁ = y₂) :=