From 352ecfe114946c903338006dd3287cb5a9955ff2 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 24 Mar 2022 22:53:04 +0000
Subject: [PATCH] feat(combinatorics/simple_graph/{connectivity,metric}):
 `connected` and `dist` (#12574)

Co-authored-by: Vincent Beffara <vbeffara@gmail.com>
---
 .../simple_graph/connectivity.lean            | 112 ++++++++++++++++-
 src/combinatorics/simple_graph/metric.lean    | 117 ++++++++++++++++++
 2 files changed, 227 insertions(+), 2 deletions(-)
 create mode 100644 src/combinatorics/simple_graph/metric.lean

diff --git a/src/combinatorics/simple_graph/connectivity.lean b/src/combinatorics/simple_graph/connectivity.lean
index 31bb3954eb89b..9db4fa2c809bf 100644
--- a/src/combinatorics/simple_graph/connectivity.lean
+++ b/src/combinatorics/simple_graph/connectivity.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import combinatorics.simple_graph.basic
+import combinatorics.simple_graph.subgraph
 import data.list
 /-!
 
@@ -37,6 +38,16 @@ counterparts in [Chou1994].
 
 * `simple_graph.path`
 
+* `simple_graph.reachable` for the relation of whether there exists
+  a walk between a given pair of vertices
+
+* `simple_graph.preconnected` and `simple_graph.connected` are predicates
+  on simple graphs for whether every vertex can be reached from every other,
+  and in the latter case, whether the vertex type is nonempty.
+
+* `simple_graph.subgraph.connected` gives subgraphs the connectivity
+  predicate via `simple_graph.subgraph.coe`.
+
 ## Tags
 walks, trails, paths, circuits, cycles
 
@@ -194,6 +205,18 @@ by simp [reverse]
 @[simp] lemma length_reverse {u v : V} (p : G.walk u v) : p.reverse.length = p.length :=
 by simp [reverse]
 
+lemma eq_of_length_eq_zero : Π {u v : V} {p : G.walk u v}, p.length = 0 → u = v
+| _ _ nil _ := rfl
+
+@[simp] lemma exists_length_eq_zero_iff {u v : V} : (∃ (p : G.walk u v), p.length = 0) ↔ u = v :=
+begin
+  split,
+  { rintro ⟨p, hp⟩,
+    exact eq_of_length_eq_zero hp, },
+  { rintro rfl,
+    exact ⟨nil, 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]
@@ -417,7 +440,7 @@ structure is_circuit {u : V} (p : G.walk u u) extends to_trail : is_trail p : Pr
 
 /-- A *cycle* at `u : V` is a circuit at `u` whose only repeating vertex
 is `u` (which appears exactly twice). -/
-structure is_cycle [decidable_eq V] {u : V} (p : G.walk u u)
+structure is_cycle {u : V} (p : G.walk u u)
   extends to_circuit : is_circuit p : Prop :=
 (support_nodup : p.support.tail.nodup)
 
@@ -430,7 +453,7 @@ lemma is_path.mk' {u v : V} {p : G.walk u v} (h : p.support.nodup) : is_path p :
 lemma is_path_def {u v : V} (p : G.walk u v) : p.is_path ↔ p.support.nodup :=
 ⟨is_path.support_nodup, is_path.mk'⟩
 
-lemma is_cycle_def [decidable_eq V] {u : V} (p : G.walk u u) :
+lemma is_cycle_def {u : V} (p : G.walk u u) :
   p.is_cycle ↔ is_trail p ∧ p ≠ nil ∧ p.support.tail.nodup :=
 iff.intro (λ h, ⟨h.1.1, h.1.2, h.2⟩) (λ h, ⟨⟨h.1, h.2.1⟩, h.2.2⟩)
 
@@ -781,4 +804,89 @@ edges_bypass_subset _
 
 end walk
 
+/-! ## `reachable` and `connected` -/
+
+/-- Two vertices are *reachable* if there is a walk between them.
+This is equivalent to `relation.refl_trans_gen` of `G.adj`.
+See `simple_graph.reachable_iff_refl_trans_gen`. -/
+def reachable (u v : V) : Prop := nonempty (G.walk u v)
+
+variables {G}
+
+lemma reachable_iff_nonempty_univ {u v : V} :
+  G.reachable u v ↔ (set.univ : set (G.walk u v)).nonempty :=
+set.nonempty_iff_univ_nonempty
+
+protected lemma reachable.elim {p : Prop} {u v : V}
+  (h : G.reachable u v) (hp : G.walk u v → p) : p :=
+nonempty.elim h hp
+
+protected lemma reachable.elim_path {p : Prop} {u v : V}
+  (h : G.reachable u v) (hp : G.path u v → p) : p :=
+begin
+  classical,
+  exact h.elim (λ q, hp q.to_path),
+end
+
+@[refl] protected lemma reachable.refl {u : V} : G.reachable u u := by { fsplit, refl }
+
+@[symm] protected lemma reachable.symm {u v : V} (huv : G.reachable u v) : G.reachable v u :=
+huv.elim (λ p, ⟨p.reverse⟩)
+
+@[trans] protected lemma reachable.trans {u v w : V}
+  (huv : G.reachable u v) (hvw : G.reachable v w) :
+  G.reachable u w :=
+huv.elim (λ puv, hvw.elim (λ pvw, ⟨puv.append pvw⟩))
+
+lemma reachable_iff_refl_trans_gen (u v : V) :
+  G.reachable u v ↔ relation.refl_trans_gen G.adj u v :=
+begin
+  split,
+  { rintro ⟨h⟩,
+    induction h,
+    { refl, },
+    { exact (relation.refl_trans_gen.single h_h).trans h_ih, }, },
+  { intro h,
+    induction h with _ _ _ ha hr,
+    { refl, },
+    { exact reachable.trans hr ⟨walk.cons ha walk.nil⟩, }, },
+end
+
+variables (G)
+
+lemma reachable_is_equivalence : equivalence G.reachable :=
+mk_equivalence _ (@reachable.refl _ G) (@reachable.symm _ G) (@reachable.trans _ G)
+
+/-- The equivalence relation on vertices given by `simple_graph.reachable`. -/
+def reachable_setoid : setoid V := setoid.mk _ G.reachable_is_equivalence
+
+/-- A graph is preconnected if every pair of vertices is reachable from one another. -/
+def preconnected : Prop := ∀ (u v : V), G.reachable u v
+
+/-- A graph is connected if it's preconnected and contains at least one vertex.
+This follows the convention observed by mathlib that something is connected iff it has
+exactly one connected component.
+
+There is a `has_coe_to_fun` instance so that `h u v` can be used instead
+of `h.preconnected u v`. -/
+@[protect_proj]
+structure connected : Prop :=
+(preconnected : G.preconnected)
+(nonempty : nonempty V)
+
+instance : has_coe_to_fun G.connected (λ _, Π (u v : V), G.reachable u v) :=
+⟨λ h, h.preconnected⟩
+
+/-- A subgraph is connected if it is connected as a simple graph. -/
+abbreviation subgraph.connected {G : simple_graph V} (H : G.subgraph) : Prop := H.coe.connected
+
+variables {G}
+
+lemma preconnected.set_univ_walk_nonempty (hconn : G.preconnected) (u v : V) :
+  (set.univ : set (G.walk u v)).nonempty :=
+by { rw ← set.nonempty_iff_univ_nonempty, exact hconn u v }
+
+lemma connected.set_univ_walk_nonempty (hconn : G.connected) (u v : V) :
+  (set.univ : set (G.walk u v)).nonempty := hconn.preconnected.set_univ_walk_nonempty u v
+
 end simple_graph
diff --git a/src/combinatorics/simple_graph/metric.lean b/src/combinatorics/simple_graph/metric.lean
new file mode 100644
index 0000000000000..9bc039fd1a880
--- /dev/null
+++ b/src/combinatorics/simple_graph/metric.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2022 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller, Vincent Beffara
+-/
+import combinatorics.simple_graph.connectivity
+import data.nat.lattice
+
+/-!
+# Graph metric
+
+This module defines the `simple_graph.dist` function, which takes
+pairs of vertices to the length of the shortest walk between them.
+
+## Main definitions
+
+- `simple_graph.dist` is the graph metric.
+
+## Todo
+
+- Provide an additional computable version of `simple_graph.dist`
+  for when `G` is connected.
+
+- Evaluate `nat` vs `enat` for the codomain of `dist`, or potentially
+  having an additional `edist` when the objects under consideration are
+  disconnected graphs.
+
+- When directed graphs exist, a directed notion of distance,
+  likely `enat`-valued.
+
+## Tags
+
+graph metric, distance
+
+-/
+
+namespace simple_graph
+variables {V : Type*} (G : simple_graph V)
+
+/-! ## Metric -/
+
+/-- The distance between two vertices is the length of the shortest walk between them.
+If no such walk exists, this uses the junk value of `0`. -/
+noncomputable
+def dist (u v : V) : ℕ := Inf (set.range (walk.length : G.walk u v → ℕ))
+
+variables {G}
+
+protected
+lemma reachable.exists_walk_of_dist {u v : V} (hr : G.reachable u v) :
+  ∃ (p : G.walk u v), p.length = G.dist u v :=
+nat.Inf_mem (set.range_nonempty_iff_nonempty.mpr hr)
+
+protected
+lemma connected.exists_walk_of_dist (hconn : G.connected) (u v : V) :
+  ∃ (p : G.walk u v), p.length = G.dist u v :=
+(hconn u v).exists_walk_of_dist
+
+lemma dist_le {u v : V} (p : G.walk u v) : G.dist u v ≤ p.length := nat.Inf_le ⟨p, rfl⟩
+
+@[simp]
+lemma dist_eq_zero_iff_eq_or_not_reachable {u v : V} : G.dist u v = 0 ↔ u = v ∨ ¬ G.reachable u v :=
+by simp [dist, nat.Inf_eq_zero, reachable]
+
+lemma dist_self {v : V} : dist G v v = 0 := by simp
+
+protected
+lemma reachable.dist_eq_zero_iff {u v : V} (hr : G.reachable u v) :
+  G.dist u v = 0 ↔ u = v := by simp [hr]
+
+protected
+lemma reachable.pos_dist_of_ne {u v : V} (h : G.reachable u v) (hne : u ≠ v) : 0 < G.dist u v :=
+nat.pos_of_ne_zero (by simp [h, hne])
+
+protected
+lemma connected.dist_eq_zero_iff (hconn : G.connected) {u v : V} :
+  G.dist u v = 0 ↔ u = v := by simp [hconn u v]
+
+protected
+lemma connected.pos_dist_of_ne {u v : V} (hconn : G.connected) (hne : u ≠ v) : 0 < G.dist u v :=
+nat.pos_of_ne_zero (by simp [hconn.dist_eq_zero_iff, hne])
+
+lemma dist_eq_zero_of_not_reachable {u v : V} (h : ¬ G.reachable u v) : G.dist u v = 0 :=
+by simp [h]
+
+lemma nonempty_of_pos_dist {u v : V} (h : 0 < G.dist u v) :
+  (set.univ : set (G.walk u v)).nonempty :=
+by simpa [set.range_nonempty_iff_nonempty, set.nonempty_iff_univ_nonempty]
+     using nat.nonempty_of_pos_Inf h
+
+protected
+lemma connected.dist_triangle (hconn : G.connected) {u v w : V} :
+  G.dist u w ≤ G.dist u v + G.dist v w :=
+begin
+  obtain ⟨p, hp⟩ := hconn.exists_walk_of_dist u v,
+  obtain ⟨q, hq⟩ := hconn.exists_walk_of_dist v w,
+  rw [← hp, ← hq, ← walk.length_append],
+  apply dist_le,
+end
+
+private
+lemma dist_comm_aux {u v : V} (h : G.reachable u v) : G.dist u v ≤ G.dist v u :=
+begin
+  obtain ⟨p, hp⟩ := h.symm.exists_walk_of_dist,
+  rw [← hp, ← walk.length_reverse],
+  apply dist_le,
+end
+
+lemma dist_comm {u v : V} : G.dist u v = G.dist v u :=
+begin
+  by_cases h : G.reachable u v,
+  { apply le_antisymm (dist_comm_aux h) (dist_comm_aux h.symm), },
+  { have h' : ¬ G.reachable v u := λ h', absurd h'.symm h,
+    simp [h, h', dist_eq_zero_of_not_reachable], },
+end
+
+end simple_graph