[Merged by Bors] - feat(combinatorics/simple_graph): boolean_algebra for simple_graphs.

src/combinatorics/simple_graph/basic.lean

@@ -35,6 +35,9 @@ finitely many vertices.
   graph isomorphisms. Note that a graph embedding is a stronger notion than an
   injective graph homomorphism, since its image is an induced subgraph.
 
+* `boolean_algebra` instance: Under the subgraph relation, `simple_graph` forms a `boolean_algebra`.
+  In other words, this is the lattice of spanning subgraphs of the complete graph.
+
 ## Notations
 
 * `→g`, `↪g`, and `≃g` for graph homomorphisms, graph embeddings, and graph isomorphisms,
@@ -57,7 +60,7 @@ finitely many vertices.
 
 ## Todo
 
-* The `bounded_lattice (simple_graph V)` instance.
+* Upgrade `simple_graph.boolean_algebra` to a `complete_boolean_algebra`.
 
 * This is the simplest notion of an unoriented graph.  This should
 eventually fit into a more complete combinatorics hierarchy which
@@ -97,36 +100,138 @@ lemma simple_graph.from_rel_adj {V : Type u} (r : V → V → Prop) (v w : V) :
   (simple_graph.from_rel r).adj v w ↔ v ≠ w ∧ (r v w ∨ r w v) :=
 iff.rfl
 
+/-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices
+adjacent. In `mathlib`, this is usually referred to as `⊤`. -/
+def complete_graph (V : Type u) : simple_graph V := { adj := ne }
+
+/-- The graph with no edges on a given vertex type `V`. `mathlib` prefers the notation `⊥`. -/
+def empty_graph (V : Type u) : simple_graph V := { adj := λ i j, false }
+
+namespace simple_graph
+
+variables {V : Type u} {W : Type v} {X : Type w} (G : simple_graph V) (G' : simple_graph W)
+
+@[simp] lemma irrefl {v : V} : ¬G.adj v v := G.loopless v
+
+lemma adj_comm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩
+
+@[symm] lemma adj_symm {u v : V} (h : G.adj u v) : G.adj v u := G.sym h
+
+lemma ne_of_adj {a b : V} (hab : G.adj a b) : a ≠ b :=
+by { rintro rfl, exact G.irrefl hab }
+
+section order
+
+/-- The relation that one `simple_graph` is a subgraph of another.
+Note that this should be spelled `≤`. -/
+def is_subgraph (x y : simple_graph V) : Prop := ∀ ⦃v w : V⦄, x.adj v w → y.adj v w
+
+instance : has_le (simple_graph V) := ⟨is_subgraph⟩
+
+@[simp] lemma is_subgraph_eq_le : (is_subgraph : simple_graph V → simple_graph V → Prop) = (≤) := rfl
+
+/-- The supremum of two graphs `x ⊔ y` has edges where either `x` or `y` have edges. -/
+instance : has_sup (simple_graph V) := ⟨λ x y,
+  { adj := x.adj ⊔ y.adj,
+    sym := λ v w h, by rwa [sup_apply, sup_apply, x.adj_comm, y.adj_comm] }⟩
+
+@[simp] lemma sup_adj (x y : simple_graph V) (v w : V) : (x ⊔ y).adj v w ↔ x.adj v w ∨ y.adj v w :=
+iff.rfl
+
+/-- The infinum of two graphs `x ⊓ y` has edges where both `x` and `y` have edges. -/
+instance : has_inf (simple_graph V) := ⟨λ x y,
+  { adj := x.adj ⊓ y.adj,
+    sym := λ v w h, by rwa [inf_apply, inf_apply, x.adj_comm, y.adj_comm] }⟩
+
+@[simp] lemma inf_adj (x y : simple_graph V) (v w : V) : (x ⊓ y).adj v w ↔ x.adj v w ∧ y.adj v w :=
+iff.rfl
+
 /--
-The complete graph on a type `V` is the simple graph with all pairs of distinct vertices adjacent.
+We define `cGᶜ` to be the `simple_graph V` such that no two adjacent vertices in `G`
+are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
+(still ensuring that vertices are not adjacent to themselves).
 -/
-def complete_graph (V : Type u) : simple_graph V :=
-{ adj := ne }
+instance : has_compl (simple_graph V) := ⟨λ G,
+  { adj := λ v w, v ≠ w ∧ ¬G.adj v w,
+    sym := λ v w ⟨hne, _⟩, ⟨hne.symm, by rwa adj_comm⟩,
+    loopless := λ v ⟨hne, _⟩, (hne rfl).elim }⟩
 
-instance (V : Type u) : inhabited (simple_graph V) :=
-⟨complete_graph V⟩
+@[simp] lemma compl_adj (G : simple_graph V) (v w : V) : Gᶜ.adj v w ↔ v ≠ w ∧ ¬G.adj v w := iff.rfl
 
-instance complete_graph_adj_decidable (V : Type u) [decidable_eq V] :
-  decidable_rel (complete_graph V).adj :=
-λ v w, not.decidable
+/-- The difference of two graphs `x / y` has the edges of `x` with the edges of `y` removed. -/
+instance : has_sdiff (simple_graph V) := ⟨λ x y,
+  { adj := x.adj \ y.adj,
+    sym := λ v w h, by change x.adj w v ∧ ¬ y.adj w v; rwa [x.adj_comm, y.adj_comm] }⟩
 
-/-- The graph with no edges on a given vertex type `V`. -/
-def empty_graph (V : Type u) : simple_graph V :=
-{ adj := λ i j, false }
+@[simp] lemma sdiff_adj (x y : simple_graph V) (v w : V) :
+  (x \ y).adj v w ↔ (x.adj v w ∧ ¬ y.adj v w) := iff.rfl
 
-namespace simple_graph
+instance : boolean_algebra (simple_graph V) :=
+{ le := (≤),
+  sup := (⊔),
+  inf := (⊓),
+  compl := has_compl.compl,
+  sdiff := (\),
+  top := complete_graph V,
+  bot := empty_graph V,
+  le_top := λ x v w h, x.ne_of_adj h,
+  bot_le := λ x v w h, h.elim,
+  sup_le := λ x y z hxy hyz v w h, h.cases_on (λ h, hxy h) (λ h, hyz h),
+  sdiff_eq := λ x y, by { ext v w, refine ⟨λ h, ⟨h.1, ⟨_, h.2⟩⟩, λ h, ⟨h.1, h.2.2⟩⟩,
+                          rintro rfl, exact x.irrefl h.1 },
+  sup_inf_sdiff := λ a b, by { ext v w, refine ⟨λ h, _, λ h', _⟩,
+                               obtain ⟨ha, _⟩|⟨ha, _⟩ := h; exact ha,
+                               by_cases b.adj v w; exact or.inl ⟨h', h⟩ <|> exact or.inr ⟨h', h⟩ },
+  inf_inf_sdiff := λ a b, by { ext v w, exact ⟨λ ⟨⟨_, hb⟩,⟨_, hb'⟩⟩, hb' hb, λ h, h.elim⟩ },
+  le_sup_left := λ x y v w h, or.inl h,
+  le_sup_right := λ x y v w h, or.inr h,
+  le_inf := λ x y z hxy hyz v w h, ⟨hxy h, hyz h⟩,
+  le_sup_inf := λ a b c v w h, or.dcases_on h.2 or.inl $
+    or.dcases_on h.1 (λ h _, or.inl h) $ λ hb hc, or.inr ⟨hb, hc⟩,
+  inf_compl_le_bot := λ a v w h, false.elim $ h.2.2 h.1,
+  top_le_sup_compl := λ a v w ne, by { by_cases a.adj v w, exact or.inl h, exact or.inr ⟨ne, h⟩ },
+  inf_le_left := λ x y v w h, h.1,
+  inf_le_right := λ x y v w h, h.2,
+  .. partial_order.lift adj ext }
 
-variables {V : Type u} {W : Type v} {X : Type w} (G : simple_graph V) (G' : simple_graph W)
+@[simp] lemma top_adj (v w : V) : (⊤ : simple_graph V).adj v w ↔ v ≠ w := iff.rfl
+
+@[simp] lemma bot_adj (v w : V) : (⊥ : simple_graph V).adj v w ↔ false := iff.rfl
+
+@[simp] lemma complete_graph_eq_top (V : Type u) : complete_graph V = ⊤ := rfl
+
+@[simp] lemma empty_graph_eq_bot (V : Type u) : empty_graph V = ⊥ := rfl
+
+instance (V : Type u) : inhabited (simple_graph V) := ⟨⊤⟩
+
+section decidable
+
+variables (V) (H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj]
+
+instance bot.adj_decidable   : decidable_rel (⊥ : simple_graph V).adj := λ v w, decidable.false
+
+instance sup.adj_decidable   : decidable_rel (G ⊔ H).adj := λ v w, or.decidable
+
+instance inf.adj_decidable   : decidable_rel (G ⊓ H).adj := λ v w, and.decidable
+
+instance sdiff.adj_decidable : decidable_rel (G \ H).adj := λ v w, and.decidable
+
+variable [decidable_eq V]
+
+instance top.adj_decidable   : decidable_rel (⊤ : simple_graph V).adj :=  λ v w, not.decidable
+
+instance compl.adj_decidable : decidable_rel Gᶜ.adj := λ v w, and.decidable
+
+end decidable
+
+end order
 
 /-- `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)
 
 instance neighbor_set.mem_decidable (v : V) [decidable_rel G.adj] :
   decidable_pred (∈ G.neighbor_set v) := by { unfold neighbor_set, apply_instance }
 
-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`.
@@ -195,12 +300,6 @@ set.mem_to_finset
   (univ : finset G.edge_set).card = G.edge_finset.card :=
 fintype.card_of_subtype G.edge_finset (mem_edge_finset _)
 
-@[simp] lemma irrefl {v : V} : ¬G.adj v v := G.loopless v
-
-lemma adj_comm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩
-
-@[symm] lemma adj_symm {u v : V} (h : G.adj u v) : G.adj v u := G.sym h
-
 @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w :=
 iff.rfl
 
@@ -221,6 +320,24 @@ begin
   { rintro rfl, use [he, h, he], apply sym2.mem_other_mem, },
 end
 
+lemma compl_neighbor_set_disjoint (G : simple_graph V) (v : V) :
+  disjoint (G.neighbor_set v) (Gᶜ.neighbor_set v) :=
+begin
+  rw set.disjoint_iff,
+  rintro w ⟨h, h'⟩,
+  rw [mem_neighbor_set, compl_adj] at h',
+  exact h'.2 h,
+end
+
+lemma neighbor_set_union_compl_neighbor_set_eq (G : simple_graph V) (v : V) :
+  G.neighbor_set v ∪ Gᶜ.neighbor_set v = {v}ᶜ :=
+begin
+  ext w,
+  have h := @ne_of_adj _ G,
+  simp_rw [set.mem_union, mem_neighbor_set, compl_adj, set.mem_compl_eq, set.mem_singleton_iff],
+  tauto,
+end
+
 /--
 The set of common neighbors between two vertices `v` and `w` in a graph `G` is the
 intersection of the neighbor sets of `v` and `w`.
@@ -370,14 +487,14 @@ by { ext, simp }
 
 @[simp]
 lemma complete_graph_degree [decidable_eq V] (v : V) :
-  (complete_graph V).degree v = fintype.card V - 1 :=
+  (⊤ : simple_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) :=
+  (⊤ : simple_graph V).is_regular_of_degree (fintype.card V - 1) :=
 by { intro v, simp }
 
 /--
@@ -537,66 +654,6 @@ end
 
 end finite
 
-section complement
-
-/-!
-## Complement of a simple graph
-
-This section contains definitions and lemmas concerning the complement of a simple graph.
--/
-
-/--
-We define `compl G` to be the `simple_graph V` such that no two adjacent vertices in `G`
-are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
-(still ensuring that vertices are not adjacent to themselves.)
--/
-def compl (G : simple_graph V) : simple_graph V :=
-{ adj := λ v w, v ≠ w ∧ ¬G.adj v w,
-  sym := λ v w ⟨hne, _⟩, ⟨hne.symm, by rwa adj_comm⟩,
-  loopless := λ v ⟨hne, _⟩, false.elim (hne rfl) }
-
-instance has_compl : has_compl (simple_graph V) :=
-{ compl := compl }
-
-@[simp]
-lemma compl_adj (G : simple_graph V) (v w : V) : Gᶜ.adj v w ↔ v ≠ w ∧ ¬G.adj v w := iff.rfl
-
-instance compl_adj_decidable (V : Type u) [decidable_eq V] (G : simple_graph V)
-  [decidable_rel G.adj] : decidable_rel Gᶜ.adj := λ v w, and.decidable
-
-@[simp]
-lemma compl_compl (G : simple_graph V) : Gᶜᶜ = G :=
-begin
-  ext v w,
-  split; simp only [compl_adj, not_and, not_not],
-  { exact λ ⟨hne, h⟩, h hne },
-  { intro h,
-    simpa [G.ne_of_adj h], },
-end
-
-@[simp]
-lemma compl_involutive : function.involutive (@compl V) := compl_compl
-
-lemma compl_neighbor_set_disjoint (G : simple_graph V) (v : V) :
-  disjoint (G.neighbor_set v) (Gᶜ.neighbor_set v) :=
-begin
-  rw set.disjoint_iff,
-  rintro w ⟨h, h'⟩,
-  rw [mem_neighbor_set, compl_adj] at h',
-  exact h'.2 h,
-end
-
-lemma neighbor_set_union_compl_neighbor_set_eq (G : simple_graph V) (v : V) :
-  G.neighbor_set v ∪ Gᶜ.neighbor_set v = {v}ᶜ :=
-begin
-  ext w,
-  have h := @ne_of_adj _ G,
-  simp_rw [set.mem_union, mem_neighbor_set, compl_adj, set.mem_compl_eq, set.mem_singleton_iff],
-  tauto,
-end
-
-end complement
-
 section maps
 
 /--

src/combinatorics/simple_graph/strongly_regular.lean

@@ -52,15 +52,15 @@ open finset
 /-- Complete graphs are strongly regular. Note that the parameter `m` can take any value
   for complete graphs, since there are no distinct pairs of nonadjacent vertices. -/
 lemma complete_strongly_regular (m : ℕ) :
-  (complete_graph V).is_SRG_of (fintype.card V) (fintype.card V - 1) (fintype.card V - 2) m :=
+  (⊤ : simple_graph V).is_SRG_of (fintype.card V) (fintype.card V - 1) (fintype.card V - 2) m :=
 { card := rfl,
   regular := complete_graph_degree,
   adj_common := λ v w (h : v ≠ w),
     begin
-      simp only [fintype.card_of_finset, mem_common_neighbors, complete_graph, ne.def, filter_not,
-        ←not_or_distrib, filter_eq, filter_or, card_univ_diff, mem_univ, if_pos, ←insert_eq],
+      simp only [fintype.card_of_finset, mem_common_neighbors, filter_not, ←not_or_distrib,
+                 filter_eq, filter_or, card_univ_diff, mem_univ, if_pos, ←insert_eq, top_adj],
       rw [card_insert_of_not_mem, card_singleton],
-      simpa,
+      simp [h]
     end,
   nadj_common := λ v w (h : ¬(v ≠ w) ∧ _), (h.1 h.2).elim }