feat(combinatorics): define simple graphs (#3458)

adds basic definition of `simple_graph`s



Co-authored-by: Aaron Anderson <awainverse@gmail.com>

Author: jalex-stark

src/combinatorics/simple_graph.lean

@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2020 Aaron Anderson, Jalex Stark, Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Aaron Anderson, Jalex Stark, Kyle Miller.
+-/
+import data.fintype.basic
+import data.sym2
+/-!
+# Simple graphs
+
+This module defines simple graphs on a vertex type `V` as an
+irreflexive symmetric relation.
+
+There is a basic API for locally finite graphs and for graphs with
+finitely many vertices.
+
+## Main definitions
+
+* `simple_graph` is a structure for symmetric, irreflexive relations
+
+* `neighbor_set` is the `set` of vertices adjacent to a given vertex
+
+* `neighbor_finset` is the `finset` of vertices adjacent to a given vertex,
+   if `neighbor_set` is finite
+
+## Implementation notes
+
+* A locally finite graph is one with instances `∀ v, fintype (G.neighbor_set v)`.
+
+* Given instances `decidable_rel G.adj` and `fintype V`, then the graph
+is locally finite, too.
+
+TODO: This is the simplest notion of an unoriented graph.  This should
+eventually fit into a more complete combinatorics hierarchy which
+includes multigraphs and directed graphs.  We begin with simple graphs
+in order to start learning what the combinatorics hierarchy should
+look like.
+
+TODO: Part of this would include defining, for example, subgraphs of a
+simple graph.
+
+-/
+open finset
+universe u
+
+/--
+A simple graph is an irreflexive symmetric relation `adj` on a vertex type `V`.
+The relation describes which pairs of vertices are adjacent.
+There is exactly one edge for every pair of adjacent edges;
+see `simple_graph.edge_set` for the corresponding edge set.
+-/
+structure simple_graph (V : Type u) :=
+(adj : V → V → Prop)
+(sym : symmetric adj . obviously)
+(loopless : irreflexive adj . obviously)
+
+/--
+The complete graph on a type `V` is the simple graph with all pairs of distinct vertices adjacent.
+-/
+def complete_graph (V : Type u) : simple_graph V :=
+{ adj := ne }
+
+instance (V : Type u) : inhabited (simple_graph V) :=
+⟨complete_graph V⟩
+
+instance complete_graph_adj_decidable (V : Type u) [decidable_eq V] :
+  decidable_rel (complete_graph V).adj :=
+by { dsimp [complete_graph], apply_instance }
+
+namespace simple_graph
+variables {V : Type u} (G : simple_graph V)
+
+/-- `G.neighbor_set v` is the set of vertices adjacent to `v` in `G`. -/
+def neighbor_set (v : V) : set V := set_of (G.adj v)
+
+lemma ne_of_adj {a b : V} (hab : G.adj a b) : a ≠ b :=
+by { rintro rfl, exact G.loopless a hab }
+
+/--
+The edges of G consist of the unordered pairs of vertices related by
+`G.adj`.
+-/
+def edge_set : set (sym2 V) := sym2.from_rel G.sym
+
+@[simp]
+lemma mem_edge_set {v w : V} : ⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w :=
+by refl
+
+/--
+Two vertices are adjacent iff there is an edge between them.  The
+condition `v ≠ w` ensures they are different endpoints of the edge,
+which is necessary since when `v = w` the existential
+`∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e` is satisfied by every edge
+incident to `v`.
+-/
+lemma adj_iff_exists_edge {v w : V} :
+  G.adj v w ↔ v ≠ w ∧ ∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e :=
+begin
+  split, { intro, split, { exact G.ne_of_adj a, }, {use ⟦(v,w)⟧, simpa} },
+  { rintro ⟨hne, e, he, hv⟩,
+    rw sym2.elems_iff_eq hne at hv,
+    subst e,
+    rwa mem_edge_set at he, }
+end
+
+lemma edge_other_ne {e : sym2 V} (he : e ∈ G.edge_set) {v : V} (h : v ∈ e) : h.other ≠ v :=
+begin
+  erw [← sym2.mem_other_spec h, sym2.eq_swap] at he,
+  exact G.ne_of_adj he,
+end
+
+instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] :
+  fintype G.edge_set := by { dunfold edge_set, exact subtype.fintype _ }
+
+/--
+The `edge_set` of the graph as a `finset`.
+-/
+def edge_finset [decidable_eq V] [fintype V] [decidable_rel G.adj] : finset (sym2 V) :=
+set.to_finset G.edge_set
+
+@[simp] lemma mem_edge_finset [decidable_eq V] [fintype V] [decidable_rel G.adj] (e : sym2 V) :
+  e ∈ G.edge_finset ↔ e ∈ G.edge_set :=
+by { dunfold edge_finset, simp }
+
+@[simp] lemma irrefl {v : V} : ¬G.adj v v := G.loopless v
+
+@[symm] lemma edge_symm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩
+
+@[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w :=
+by tauto
+
+section finite_at
+
+/-!
+## Finiteness at a vertex
+
+This section contains definitions and lemmas concerning vertices that
+have finitely many adjacent vertices.  We denote this condition by
+`fintype (G.neighbor_set v)`.
+
+We define `G.neighbor_finset v` to be the `finset` version of `G.neighbor_set v`.
+Use `neighbor_finset_eq_filter` to rewrite this definition as a `filter`.
+-/
+
+variables (v : V) [fintype (G.neighbor_set v)]
+/--
+`G.neighbors v` is the `finset` version of `G.adj v` in case `G` is
+locally finite at `v`.
+-/
+def neighbor_finset : finset V := (G.neighbor_set v).to_finset
+
+@[simp] lemma mem_neighbor_finset (w : V) :
+  w ∈ G.neighbor_finset v ↔ G.adj v w :=
+by simp [neighbor_finset]
+
+/--
+`G.degree v` is the number of vertices adjacent to `v`.
+-/
+def degree : ℕ := (G.neighbor_finset v).card
+
+@[simp]
+lemma card_neighbor_set_eq_degree : fintype.card (G.neighbor_set v) = G.degree v :=
+by simp [degree, neighbor_finset]
+
+end finite_at
+
+section locally_finite
+
+/--
+A graph is locally finite if every vertex has a finite neighbor set.
+-/
+@[reducible]
+def locally_finite := Π (v : V), fintype (G.neighbor_set v)
+
+variable [locally_finite G]
+
+/--
+A locally finite simple graph is regular of degree `d` if every vertex has degree `d`.
+-/
+def is_regular_of_degree (d : ℕ) : Prop := ∀ (v : V), G.degree v = d
+
+end locally_finite
+
+section finite
+
+variables [fintype V]
+
+instance neighbor_set_fintype [decidable_rel G.adj] (v : V) : fintype (G.neighbor_set v) :=
+@subtype.fintype _ _ (by { simp_rw mem_neighbor_set, apply_instance }) _
+
+lemma neighbor_finset_eq_filter {v : V} [decidable_rel G.adj] :
+  G.neighbor_finset v = finset.univ.filter (G.adj v) :=
+by { ext, simp }
+
+@[simp]
+lemma complete_graph_degree [decidable_eq V] (v : V) :
+  (complete_graph V).degree v = fintype.card V - 1 :=
+begin
+  convert univ.card.pred_eq_sub_one,
+  erw [degree, neighbor_finset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v)],
+end
+
+lemma complete_graph_is_regular [decidable_eq V] :
+  (complete_graph V).is_regular_of_degree (fintype.card V - 1) :=
+by { intro v, simp }
+
+end finite
+
+end simple_graph

src/data/sym2.lean

@@ -41,13 +41,14 @@ term of the symmetric square.
 symmetric square, unordered pairs, symmetric powers
 -/
 
+universe u
+variables {α : Type u}
 namespace sym2
-variables {α : Type*}
 
 /--
 This is the relation capturing the notion of pairs equivalent up to permutations.
 -/
-inductive rel (α : Type*) : (α × α) → (α × α) → Prop
+inductive rel (α : Type u) : (α × α) → (α × α) → Prop
 | refl (x y : α) : rel (x, y) (x, y)
 | swap (x y : α) : rel (x, y) (y, x)
 
@@ -61,7 +62,7 @@ by { intros a b, cases_matching* rel _ _ _; apply rel.refl <|> apply rel.swap }
 
 lemma rel.is_equivalence : equivalence (rel α) := by tidy; apply rel.trans; assumption
 
-instance rel.setoid (α : Type*) : setoid (α × α) := ⟨rel α, rel.is_equivalence⟩
+instance rel.setoid (α : Type u) : setoid (α × α) := ⟨rel α, rel.is_equivalence⟩
 
 end sym2
 
@@ -73,11 +74,9 @@ It is equivalent in a natural way to multisets of cardinality 2 (see
 `sym2.equiv_multiset`).
 -/
 @[reducible]
-def sym2 (α : Type*) := quotient (sym2.rel.setoid α)
+def sym2 (α : Type u) := quotient (sym2.rel.setoid α)
 
 namespace sym2
-universe u
-variables {α : Type u}
 
 lemma eq_swap {a b : α} : ⟦(a, b)⟧ = ⟦(b, a)⟧ :=
 by { rw quotient.eq, apply rel.swap }
@@ -114,6 +113,7 @@ def mem (x : α) (z : sym2 α) : Prop :=
 instance : has_mem α (sym2 α) := ⟨mem⟩
 
 lemma mk_has_mem (x y : α) : x ∈ ⟦(x, y)⟧ := ⟨y, rfl⟩
+lemma mk_has_mem_right (x y : α) : y ∈ ⟦(x, y)⟧ := by { rw eq_swap, apply mk_has_mem }
 
 /--
 This is a type-valued version of the membership predicate `mem` that contains the other
@@ -167,9 +167,21 @@ begin
   { cases h; rw [h.1, h.2], rw eq_swap }
 end
 
-lemma mem_iff {a b c : α} : a ∈ ⟦(b, c)⟧ ↔ a = b ∨ a = c :=
+@[simp] lemma mem_iff {a b c : α} : a ∈ ⟦(b, c)⟧ ↔ a = b ∨ a = c :=
 { mp  := by { rintro ⟨_, h⟩, rw eq_iff at h, tidy },
-  mpr := by { rintro ⟨_⟩; subst a, { apply mk_has_mem }, rw eq_swap, apply mk_has_mem } }
+  mpr := by { rintro ⟨_⟩; subst a, { apply mk_has_mem }, apply mk_has_mem_right } }
+
+lemma elems_iff_eq {x y : α} {z : sym2 α} (hne : x ≠ y) :
+  x ∈ z ∧ y ∈ z ↔ z = ⟦(x, y)⟧ :=
+begin
+  split,
+  { rintros ⟨hx, hy⟩,
+    induction z, cases z with z₁ z₂,
+    apply eq_iff.mpr,
+    cases mem_iff.mp hx with hx hx; cases mem_iff.mp hy with hy hy; cc,
+    refl },
+  { rintro rfl, simp },
+end
 
 end membership
 
@@ -221,6 +233,16 @@ lemma from_rel_irreflexive {sym : symmetric r} :
               erw is_diag_iff_proj_eq at hd, erw from_rel_proj_prop at hr, tidy },
   mpr := by { intros h x hr, rw ← @from_rel_prop _ _ sym at hr, exact h hr ⟨x, rfl⟩ }}
 
+instance from_rel.decidable_as_set (sym : symmetric r) [h : decidable_rel r] :
+  decidable_pred (λ x, x ∈ sym2.from_rel sym) :=
+λ (x : sym2 α), quotient.rec_on x
+  (λ x', by { simp_rw from_rel_proj_prop, apply_instance })
+  (by tidy)
+
+instance from_rel.decidable_pred (sym : symmetric r) [h : decidable_rel r] :
+  decidable_pred (sym2.from_rel sym) :=
+by { change decidable_pred (λ x, x ∈ sym2.from_rel sym), apply_instance }
+
 end relations
 
 section sym_equiv
@@ -282,4 +304,33 @@ equiv_sym α
 
 end sym_equiv
 
+section fintype
+
+/--
+An algorithm for computing `sym2.rel`.
+-/
+def rel_bool [decidable_eq α] (x y : α × α) : bool :=
+if x.1 = y.1 then x.2 = y.2 else
+  if x.1 = y.2 then x.2 = y.1 else ff
+
+lemma rel_bool_spec [decidable_eq α] (x y : α × α) :
+  ↥(rel_bool x y) ↔ rel α x y :=
+begin
+  cases x with x₁ x₂, cases y with y₁ y₂,
+  dsimp [rel_bool], split_ifs;
+  simp only [false_iff, bool.coe_sort_ff, bool.of_to_bool_iff],
+  rotate 2, { contrapose! h, cases h; cc },
+  all_goals { subst x₁, split; intro h1,
+    { subst h1; apply sym2.rel.swap },
+    { cases h1; cc } }
+end
+
+/--
+Given `[decidable_eq α]` and `[fintype α]`, the following instance gives `fintype (sym2 α)`.
+-/
+instance (α : Type*) [decidable_eq α] : decidable_rel (sym2.rel α) :=
+λ x y, decidable_of_bool (rel_bool x y) (rel_bool_spec x y)
+
+end fintype
+
 end sym2