feat(combinatorics/simple_graph/subgraph): single-vertex and single-edge subgraphs (#16435)

Constructors for single-vertex and single-edge subgraphs along with some associated properties. Also includes dot notation improvements for `simple_graph.subgraph.adj`.

Co-authored-by: Joanna Choules <joannachoules+lean@googlemail.com>

Author: kmill

src/combinatorics/simple_graph/connectivity.lean

@@ -85,6 +85,10 @@ attribute [refl] walk.nil
 
 @[simps] instance walk.inhabited (v : V) : inhabited (G.walk v v) := ⟨walk.nil⟩
 
+/-- The one-edge walk associated to a pair of adjacent vertices. -/
+@[pattern, reducible] def adj.to_walk {G : simple_graph V} {u v : V} (h : G.adj u v) :
+  G.walk u v := walk.cons h walk.nil
+
 namespace walk
 variables {G}
 
@@ -1176,6 +1180,12 @@ begin
   exact h.elim (λ q, hp q.to_path),
 end
 
+protected lemma walk.reachable {G : simple_graph V} {u v : V} (p : G.walk u v) :
+  G.reachable u v := ⟨p⟩
+
+protected lemma adj.reachable {u v : V} (h : G.adj u v) :
+  G.reachable u v := h.to_walk.reachable
+
 @[refl] protected lemma reachable.refl (u : V) : G.reachable u u := by { fsplit, refl }
 protected lemma reachable.rfl {u : V} : G.reachable u u := reachable.refl _
 
@@ -1201,6 +1211,10 @@ begin
     { exact reachable.trans hr ⟨walk.cons ha walk.nil⟩, }, },
 end
 
+protected lemma reachable.map {G : simple_graph V} {G' : simple_graph V'}
+  (f : G →g G') {u v : V} (h : G.reachable u v) : G'.reachable (f u) (f v) :=
+h.elim (λ p, ⟨p.map f⟩)
+
 variables (G)
 
 lemma reachable_is_equivalence : equivalence G.reachable :=
@@ -1214,7 +1228,7 @@ def preconnected : Prop := ∀ (u v : V), G.reachable u v
 
 lemma preconnected.map {G : simple_graph V} {H : simple_graph V'} (f : G →g H) (hf : surjective f)
   (hG : G.preconnected) : H.preconnected :=
-hf.forall₂.2 $ λ a b, (hG _ _).map $ walk.map _
+hf.forall₂.2 $ λ a b, nonempty.map (walk.map _) $ hG _ _
 
 lemma iso.preconnected_iff {G : simple_graph V} {H : simple_graph V'} (e : G ≃g H) :
   G.preconnected ↔ H.preconnected :=
@@ -1308,6 +1322,24 @@ variables {G}
 /-- A subgraph is connected if it is connected as a simple graph. -/
 abbreviation subgraph.connected (H : G.subgraph) : Prop := H.coe.connected
 
+lemma singleton_subgraph_connected {v : V} : (G.singleton_subgraph v).connected :=
+begin
+  split,
+  rintros ⟨a, ha⟩ ⟨b, hb⟩,
+  simp only [singleton_subgraph_verts, set.mem_singleton_iff] at ha hb,
+  subst_vars
+end
+
+@[simp] lemma subgraph_of_adj_connected {v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).connected :=
+begin
+  split,
+  rintro ⟨a, ha⟩ ⟨b, hb⟩,
+  simp only [subgraph_of_adj_verts, set.mem_insert_iff, set.mem_singleton_iff] at ha hb,
+  obtain (rfl|rfl) := ha; obtain (rfl|rfl) := hb;
+    refl <|> { apply adj.reachable, simp },
+end
+
 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 }

src/combinatorics/simple_graph/subgraph.lean

@@ -61,9 +61,27 @@ structure subgraph {V : Type u} (G : simple_graph V) :=
 (edge_vert : ∀ {v w : V}, adj v w → v ∈ verts)
 (symm : symmetric adj . obviously)
 
+variables {V : Type u} {W : Type v}
+
+/-- The one-vertex subgraph. -/
+@[simps]
+protected def singleton_subgraph (G : simple_graph V) (v : V) : G.subgraph :=
+{ verts := {v},
+  adj := ⊥,
+  adj_sub := by simp [-set.bot_eq_empty],
+  edge_vert := by simp [-set.bot_eq_empty] }
+
+/-- The one-edge subgraph. -/
+@[simps]
+def subgraph_of_adj (G : simple_graph V) {v w : V} (hvw : G.adj v w) : G.subgraph :=
+{ verts := {v, w},
+  adj := λ a b, ⟦(v, w)⟧ = ⟦(a, b)⟧,
+  adj_sub := λ a b h, by { rw [← G.mem_edge_set, ← h], exact hvw },
+  edge_vert := λ a b h, by { apply_fun (λ e, a ∈ e) at h, simpa using h } }
+
 namespace subgraph
 
-variables {V : Type u} {W : Type v} {G : simple_graph V}
+variables {G : simple_graph V}
 
 protected lemma loopless (G' : subgraph G) : irreflexive G'.adj :=
 λ v h, G.loopless v (G'.adj_sub h)
@@ -75,6 +93,16 @@ lemma adj_comm (G' : subgraph G) (v w : V) : G'.adj v w ↔ G'.adj w v :=
 
 protected lemma adj.symm {G' : subgraph G} {u v : V} (h : G'.adj u v) : G'.adj v u := G'.symm h
 
+protected lemma adj.adj_sub {H : G.subgraph} {u v : V} (h : H.adj u v) : G.adj u v := H.adj_sub h
+
+protected lemma adj.fst_mem {H : G.subgraph} {u v : V} (h : H.adj u v) : u ∈ H.verts :=
+H.edge_vert h
+
+protected lemma adj.snd_mem {H : G.subgraph} {u v : V} (h : H.adj u v) : v ∈ H.verts :=
+h.symm.fst_mem
+
+protected lemma adj.ne {H : G.subgraph} {u v : V} (h : H.adj u v) : u ≠ v := h.adj_sub.ne
+
 /-- Coercion from `G' : subgraph G` to a `simple_graph ↥G'.verts`. -/
 @[simps] protected def coe (G' : subgraph G) : simple_graph G'.verts :=
 { adj := λ v w, G'.adj v w,
@@ -84,6 +112,10 @@ protected lemma adj.symm {G' : subgraph G} {u v : V} (h : G'.adj u v) : G'.adj v
 @[simp] lemma coe_adj_sub (G' : subgraph G) (u v : G'.verts) (h : G'.coe.adj u v) : G.adj u v :=
 G'.adj_sub h
 
+/- Given `h : H.adj u v`, then `h.coe : H.coe.adj ⟨u, _⟩ ⟨v, _⟩`. -/
+protected lemma adj.coe {H : G.subgraph} {u v : V} (h : H.adj u v) :
+  H.coe.adj ⟨u, H.edge_vert h⟩ ⟨v, H.edge_vert h.symm⟩ := h
+
 /-- A subgraph is called a *spanning subgraph* if it contains all the vertices of `G`. --/
 def is_spanning (G' : subgraph G) : Prop := ∀ (v : V), v ∈ G'.verts
 
@@ -493,7 +525,135 @@ begin
   simp only [set.mem_to_finset, mem_neighbor_set],
 end
 
-/-! ## Subgraphs of subgraphs -/
+end subgraph
+
+section mk_properties
+/-! ### Properties of `singleton_subgraph` and `subgraph_of_adj` -/
+
+variables {G : simple_graph V} {G' : simple_graph W}
+
+instance nonempty_singleton_subgraph_verts (v : V) : nonempty (G.singleton_subgraph v).verts :=
+⟨⟨v, set.mem_singleton v⟩⟩
+
+@[simp] lemma singleton_subgraph_le_iff (v : V) (H : G.subgraph) :
+  G.singleton_subgraph v ≤ H ↔ v ∈ H.verts :=
+begin
+  refine ⟨λ h, h.1 (set.mem_singleton v), _⟩,
+  intro h,
+  split,
+  { simp [h] },
+  { simp [-set.bot_eq_empty] }
+end
+
+@[simp] lemma map_singleton_subgraph (f : G →g G') {v : V} :
+  subgraph.map f (G.singleton_subgraph v) = G'.singleton_subgraph (f v) :=
+by ext; simp only [relation.map, subgraph.map_adj, singleton_subgraph_adj, pi.bot_apply,
+  exists_and_distrib_left, and_iff_left_iff_imp, is_empty.forall_iff, subgraph.map_verts,
+  singleton_subgraph_verts, set.image_singleton]
+
+@[simp] lemma neighbor_set_singleton_subgraph (v w : V) :
+  (G.singleton_subgraph v).neighbor_set w = ∅ :=
+by { ext u, refl }
+
+@[simp] lemma edge_set_singleton_subgraph (v : V) :
+  (G.singleton_subgraph v).edge_set = ∅ :=
+sym2.from_rel_bot
+
+lemma eq_singleton_subgraph_iff_verts_eq (H : G.subgraph) {v : V} :
+  H = G.singleton_subgraph v ↔ H.verts = {v} :=
+begin
+  refine ⟨λ h, by simp [h], λ h, _⟩,
+  ext,
+  { rw [h, singleton_subgraph_verts] },
+  { simp only [Prop.bot_eq_false, singleton_subgraph_adj, pi.bot_apply, iff_false],
+    intro ha,
+    have ha1 := ha.fst_mem,
+    have ha2 := ha.snd_mem,
+    rw [h, set.mem_singleton_iff] at ha1 ha2,
+    subst_vars,
+    exact ha.ne rfl },
+end
+
+instance nonempty_subgraph_of_adj_verts {v w : V} (hvw : G.adj v w) :
+  nonempty (G.subgraph_of_adj hvw).verts := ⟨⟨v, by simp⟩⟩
+
+@[simp] lemma edge_set_subgraph_of_adj {v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).edge_set = {⟦(v, w)⟧} :=
+begin
+  ext e,
+  refine e.ind _,
+  simp only [eq_comm, set.mem_singleton_iff, subgraph.mem_edge_set, subgraph_of_adj_adj,
+    iff_self, forall_2_true_iff],
+end
+
+lemma subgraph_of_adj_symm {v w : V} (hvw : G.adj v w) :
+  G.subgraph_of_adj hvw.symm = G.subgraph_of_adj hvw :=
+by ext; simp [or_comm, and_comm]
+
+@[simp] lemma map_subgraph_of_adj (f : G →g G')
+  {v w : V} (hvw : G.adj v w) :
+  subgraph.map f (G.subgraph_of_adj hvw) = G'.subgraph_of_adj (f.map_adj hvw) :=
+begin
+  ext,
+  { simp only [subgraph.map_verts, subgraph_of_adj_verts, set.mem_image,
+      set.mem_insert_iff, set.mem_singleton_iff],
+    split,
+    { rintro ⟨u, rfl|rfl, rfl⟩; simp },
+    { rintro (rfl|rfl),
+      { use v, simp },
+      { use w, simp } } },
+  { simp only [relation.map, subgraph.map_adj, subgraph_of_adj_adj, quotient.eq, sym2.rel_iff],
+    split,
+    { rintro ⟨a, b, (⟨rfl,rfl⟩|⟨rfl,rfl⟩), rfl, rfl⟩; simp },
+    { rintro (⟨rfl,rfl⟩|⟨rfl,rfl⟩),
+      { use [v, w], simp },
+      { use [w, v], simp } } }
+end
+
+lemma neighbor_set_subgraph_of_adj_subset {u v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).neighbor_set u ⊆ {v, w} :=
+(G.subgraph_of_adj hvw).neighbor_set_subset_verts _
+
+@[simp] lemma neighbor_set_fst_subgraph_of_adj {v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).neighbor_set v = {w} :=
+begin
+  ext u,
+  suffices : w = u ↔ u = w, by simpa [hvw.ne.symm] using this,
+  rw eq_comm,
+end
+
+@[simp] lemma neighbor_set_snd_subgraph_of_adj {v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).neighbor_set w = {v} :=
+begin
+  rw subgraph_of_adj_symm hvw.symm,
+  exact neighbor_set_fst_subgraph_of_adj hvw.symm,
+end
+
+@[simp] lemma neighbor_set_subgraph_of_adj_of_ne_of_ne {u v w : V} (hvw : G.adj v w)
+  (hv : u ≠ v) (hw : u ≠ w) :
+  (G.subgraph_of_adj hvw).neighbor_set u = ∅ :=
+by { ext, simp [hv.symm, hw.symm] }
+
+lemma neighbor_set_subgraph_of_adj [decidable_eq V] {u v w : V} (hvw : G.adj v w) :
+  (G.subgraph_of_adj hvw).neighbor_set u =
+  (if u = v then {w} else ∅) ∪ (if u = w then {v} else ∅) :=
+by split_ifs; subst_vars; simp [*]
+
+lemma singleton_subgraph_fst_le_subgraph_of_adj {u v : V} {h : G.adj u v} :
+  G.singleton_subgraph u ≤ G.subgraph_of_adj h :=
+by split; simp [-set.bot_eq_empty]
+
+lemma singleton_subgraph_snd_le_subgraph_of_adj {u v : V} {h : G.adj u v} :
+  G.singleton_subgraph v ≤ G.subgraph_of_adj h :=
+by split; simp [-set.bot_eq_empty]
+
+end mk_properties
+
+namespace subgraph
+
+variables {G : simple_graph V}
+
+/-! ### Subgraphs of subgraphs -/
 
 /-- Given a subgraph of a subgraph of `G`, construct a subgraph of `G`. -/
 @[reducible]
@@ -519,7 +679,7 @@ lemma coe_subgraph_injective (G' : G.subgraph) :
   function.injective (subgraph.coe_subgraph : G'.coe.subgraph → G.subgraph) :=
 function.left_inverse.injective restrict_coe_subgraph
 
-/-! ## Edge deletion -/
+/-! ### Edge deletion -/
 
 /-- Given a subgraph `G'` and a set of vertex pairs, remove all of the corresponding edges
 from its edge set, if present.
@@ -602,7 +762,7 @@ spanning_coe_le_of_le (delete_edges_le s)
 
 end delete_edges
 
-/-! ## Induced subgraphs -/
+/-! ### Induced subgraphs -/
 
 /- Given a subgraph, we can change its vertex set while removing any invalid edges, which
 gives induced subgraphs. See also `simple_graph.induce` for the `simple_graph` version, which,
@@ -652,6 +812,25 @@ begin
     exact λ ha, ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩ }
 end
 
+lemma singleton_subgraph_eq_induce {v : V} :
+  G.singleton_subgraph v = (⊤ : G.subgraph).induce {v} :=
+by ext; simp [-set.bot_eq_empty, Prop.bot_eq_false] { contextual := tt }
+
+lemma subgraph_of_adj_eq_induce {v w : V} (hvw : G.adj v w) :
+  G.subgraph_of_adj hvw = (⊤ : G.subgraph).induce {v, w} :=
+begin
+  ext,
+  { simp },
+  { split,
+    { intro h,
+      simp only [subgraph_of_adj_adj, quotient.eq, sym2.rel_iff] at h,
+      obtain ⟨rfl, rfl⟩|⟨rfl, rfl⟩ := h; simp [hvw, hvw.symm], },
+    { intro h,
+      simp only [induce_adj, set.mem_insert_iff, set.mem_singleton_iff, top_adj_iff] at h,
+      obtain ⟨rfl|rfl, rfl|rfl, ha⟩ := h;
+        exact (ha.ne rfl).elim <|> simp } }
+end
+
 end induce
 
 /-- Given a subgraph and a set of vertices, delete all the vertices from the subgraph,

src/data/sym/sym2.lean

@@ -363,6 +363,20 @@ lemma from_rel_proj_prop {sym : symmetric r} {z : α × α} : ⟦z⟧ ∈ from_r
 @[simp]
 lemma from_rel_prop {sym : symmetric r} {a b : α} : ⟦(a, b)⟧ ∈ from_rel sym ↔ r a b := iff.rfl
 
+lemma from_rel_bot : from_rel (λ (x y : α) z, z : symmetric ⊥) = ∅ :=
+begin
+  apply set.eq_empty_of_forall_not_mem (λ e, _),
+  refine e.ind _,
+  simp [-set.bot_eq_empty, Prop.bot_eq_false],
+end
+
+lemma from_rel_top : from_rel (λ (x y : α) z, z : symmetric ⊤) = set.univ :=
+begin
+  apply set.eq_univ_of_forall (λ e, _),
+  refine e.ind _,
+  simp [-set.top_eq_univ, Prop.top_eq_true],
+end
+
 lemma from_rel_irreflexive {sym : symmetric r} :
   irreflexive r ↔ ∀ {z}, z ∈ from_rel sym → ¬is_diag z :=
 { mp  := λ h, sym2.ind $ by { rintros a b hr (rfl : a = b), exact h _ hr },

src/order/bounded_order.lean

@@ -362,6 +362,10 @@ instance Prop.bounded_order : bounded_order Prop :=
   bot          := false,
   bot_le       := @false.elim }
 
+lemma Prop.bot_eq_false : (⊥ : Prop) = false := rfl
+
+lemma Prop.top_eq_true : (⊤ : Prop) = true := rfl
+
 instance Prop.le_is_total : is_total Prop (≤) :=
 ⟨λ p q, by { change (p → q) ∨ (q → p), tauto! }⟩