From 8b14efc1be6fcc14282bc9e0f8e3b4aea24cca10 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 15:00:21 -0500 Subject: [PATCH 01/50] added incidence set definitions and lemmas --- src/combinatorics/simple_graph/basic.lean | 113 +++++++++++++++++++++- 1 file changed, 112 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 0e8d413c55253..66aee45851788 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -23,6 +23,11 @@ finitely many vertices. * `neighbor_finset` is the `finset` of vertices adjacent to a given vertex, if `neighbor_set` is finite +* `incidence_set` is the `set` of edges containing a given vertex + +* `incidence_finset` is the `finset` of edges containing a given vertex, + if `incidence_set` is finite + ## Implementation notes * A locally finite graph is one with instances `∀ v, fintype (G.neighbor_set v)`. @@ -54,6 +59,20 @@ structure simple_graph (V : Type u) := (sym : symmetric adj . obviously) (loopless : irreflexive adj . obviously) +/-- +Construct the simple graph induced by the given relation. It +symmetrizes the relation and makes it irreflexive. +-/ +def simple_graph_from_rel {V : Type u} (r : V → V → Prop) : simple_graph V := +{ adj := λ a b, (a ≠ b) ∧ (r a b ∨ r b a), + sym := by finish, + loopless := by finish } + +@[simp] +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) := +by refl + /-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices adjacent. -/ @@ -82,6 +101,14 @@ The edges of G consist of the unordered pairs of vertices related by -/ def edge_set : set (sym2 V) := sym2.from_rel G.sym +/-- +The `incidence_set` is the set of edges incidence to a given vertex. +-/ +def incidence_set (v : V) : set (sym2 V) := {e ∈ G.edge_set | v ∈ e} + +lemma incidence_set_subset (v : V) : G.incidence_set v ⊆ G.edge_set := +by tidy + @[simp] lemma mem_edge_set {v w : V} : ⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w := by refl @@ -91,7 +118,7 @@ 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`. +incidence to `v`. -/ lemma adj_iff_exists_edge {v w : V} : G.adj v w ↔ v ≠ w ∧ ∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e := @@ -122,6 +149,10 @@ set.to_finset G.edge_set e ∈ G.edge_finset ↔ e ∈ G.edge_set := by { dunfold edge_finset, simp } +@[simp] lemma edge_set_univ_card [decidable_eq V] [fintype V] +[decidable_rel G.adj] : (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 @[symm] lemma edge_symm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩ @@ -129,6 +160,52 @@ by { dunfold edge_finset, simp } @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w := by tauto +@[simp] lemma mem_incidence_set (v w : V) : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w := +by { dsimp [incidence_set], simp } + +lemma neighbor_set_edge_prop {v w : V} (h : w ∈ G.neighbor_set v) : ⟦(v, w)⟧ ∈ G.incidence_set v := +by { rw mem_neighbor_set at h, simpa } + +lemma adj_incidence_set_inter {v : V} {e : sym2 V} (he : e ∈ G.edge_set) (h : v ∈ e) : + G.incidence_set v ∩ G.incidence_set h.other = {e} := +begin + ext e', + simp only [incidence_set, set.mem_sep_eq, set.mem_inter_eq, set.mem_singleton_iff], + split, + { intro h', rw ←sym2.mem_other_spec h, + exact (sym2.elems_iff_eq (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩, }, + { rintro rfl, use [he, h, he], apply sym2.mem_other_mem, }, +end + +section incidence +variable [decidable_eq V] + +/-- +Given an edge incidence to a particular vertex, get the other vertex on the edge. +-/ +def incidence_set_other {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' + +lemma incidence_other_prop {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : +G.incidence_set_other h ∈ G.neighbor_set v := +by { cases h, rwa [←sym2.mem_other_spec' h_right, mem_edge_set] at h_left } + +@[simp] +lemma incidence_other_neighbor_edge {v w : V} (h : w ∈ G.neighbor_set v) : + G.incidence_set_other (G.neighbor_set_edge_prop h) = w := +sym2.congr_right.mp (sym2.mem_other_spec' (G.neighbor_set_edge_prop h).right) + +/-- +There is an equivalence between the set of edges incidence to a given +vertex and the set of vertices adjacent to the vertex. +-/ +def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := +{ to_fun := λ e, ⟨G.incidence_set_other e.2, G.incidence_other_prop e.2⟩, + inv_fun := λ w, ⟨⟦(v, w.1)⟧, G.neighbor_set_edge_prop w.2⟩, + left_inv := by { intro x, dsimp [incidence_set_other], simp }, + right_inv := by { intro x, rcases x with ⟨w, hw⟩, simp, } } + +end incidence + section finite_at /-! @@ -162,6 +239,27 @@ def degree : ℕ := (G.neighbor_finset v).card lemma card_neighbor_set_eq_degree : fintype.card (G.neighbor_set v) = G.degree v := by simp [degree, neighbor_finset] +lemma degree_pos_iff_exists_adj : 0 < G.degree v ↔ ∃ w, G.adj v w := +by { simp only [degree, card_pos, finset.nonempty, mem_neighbor_finset] } + +instance incidence_set_fintype [decidable_eq V] : fintype (G.incidence_set v) := +fintype.of_equiv (G.neighbor_set v) (G.incidence_set_equiv_neighbor_set v).symm + +/-- +This is the `finset` version of `incidence_set`. +-/ +def incidence_finset [decidable_eq V] : finset (sym2 V) := (G.incidence_set v).to_finset + +@[simp] +lemma card_incidence_set_eq_degree [decidable_eq V] : + fintype.card (G.incidence_set v) = G.degree v := +by { rw fintype.card_congr (G.incidence_set_equiv_neighbor_set v), simp } + +@[simp] +lemma mem_incidence_finset [decidable_eq V] (e : sym2 V) : + e ∈ G.incidence_finset v ↔ e ∈ G.incidence_set v := +by { dunfold incidence_finset, simp } + end finite_at section locally_finite @@ -204,6 +302,19 @@ lemma complete_graph_is_regular [decidable_eq V] : (complete_graph V).is_regular_of_degree (fintype.card V - 1) := by { intro v, simp } +/-- +The minimal degree of all vertices +-/ +def min_deg (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := +finset.min' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) + +/-- +The maximal degree of all vertices +-/ +def max_deg (G : simple_graph V) [h : nonempty V] [decidable_rel G.adj]: ℕ := +finset.max' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) + + end finite end simple_graph From aae854438a9b6fea2a09e3a8a5f4ab67a5bc3809 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 15:03:28 -0500 Subject: [PATCH 02/50] forgot to give myself credit --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 66aee45851788..9df09712ac054 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -1,7 +1,7 @@ /- 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. +Author: Aaron Anderson, Jalex Stark, Kyle Miller, Alena Gusakov -/ import data.fintype.basic import data.sym2 From 95b5c857922faedc838a94da0485d0cd1108ff00 Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Wed, 2 Dec 2020 15:08:40 -0500 Subject: [PATCH 03/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Bhavik Mehta --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 9df09712ac054..8b75f9923ba6c 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -311,7 +311,7 @@ finset.min' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty /-- The maximal degree of all vertices -/ -def max_deg (G : simple_graph V) [h : nonempty V] [decidable_rel G.adj]: ℕ := +def max_deg (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := finset.max' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) From a9ef8f830dbe56dfe593f4a49d2a5f49d13b83dd Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Wed, 2 Dec 2020 15:08:48 -0500 Subject: [PATCH 04/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Bhavik Mehta --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 8b75f9923ba6c..be7c75ffd94c1 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -198,7 +198,7 @@ sym2.congr_right.mp (sym2.mem_other_spec' (G.neighbor_set_edge_prop h).right) There is an equivalence between the set of edges incidence to a given vertex and the set of vertices adjacent to the vertex. -/ -def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := +@[simps] def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := { to_fun := λ e, ⟨G.incidence_set_other e.2, G.incidence_other_prop e.2⟩, inv_fun := λ w, ⟨⟦(v, w.1)⟧, G.neighbor_set_edge_prop w.2⟩, left_inv := by { intro x, dsimp [incidence_set_other], simp }, From 4d190eba57d8d346405130ec1153e15f81eb5502 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 15:10:10 -0500 Subject: [PATCH 05/50] fixed typos in docstrings --- src/combinatorics/simple_graph/basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 9df09712ac054..34781c43b36e1 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -102,7 +102,7 @@ The edges of G consist of the unordered pairs of vertices related by def edge_set : set (sym2 V) := sym2.from_rel G.sym /-- -The `incidence_set` is the set of edges incidence to a given vertex. +The `incidence_set` is the set of edges incident to a given vertex. -/ def incidence_set (v : V) : set (sym2 V) := {e ∈ G.edge_set | v ∈ e} @@ -118,7 +118,7 @@ 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 -incidence to `v`. +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 := @@ -181,7 +181,7 @@ section incidence variable [decidable_eq V] /-- -Given an edge incidence to a particular vertex, get the other vertex on the edge. +Given an edge incident to a particular vertex, get the other vertex on the edge. -/ def incidence_set_other {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' @@ -195,7 +195,7 @@ lemma incidence_other_neighbor_edge {v w : V} (h : w ∈ G.neighbor_set v) : sym2.congr_right.mp (sym2.mem_other_spec' (G.neighbor_set_edge_prop h).right) /-- -There is an equivalence between the set of edges incidence to a given +There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex. -/ def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := From 85dd8bc09fd7eee8222bb247a0dd353d3edb4cb3 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 15:11:23 -0500 Subject: [PATCH 06/50] definition names and docstrings corrected --- src/combinatorics/simple_graph/basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 27db9271a82f8..0ceae8209b3a1 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -303,15 +303,15 @@ lemma complete_graph_is_regular [decidable_eq V] : by { intro v, simp } /-- -The minimal degree of all vertices +The minimum degree of all vertices -/ -def min_deg (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := +def min_degree (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := finset.min' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) /-- -The maximal degree of all vertices +The maximum degree of all vertices -/ -def max_deg (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := +def max_degree (G : simple_graph V) [nonempty V] [decidable_rel G.adj] : ℕ := finset.max' (univ.image (λ (v : V), G.degree v)) (nonempty.image univ_nonempty _) From fc72950d5cf81fa4b2914bafda08538c3c93cc63 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 15:32:48 -0500 Subject: [PATCH 07/50] fixed formatting --- src/combinatorics/simple_graph/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 0ceae8209b3a1..e1df5947e6990 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -149,8 +149,8 @@ set.to_finset G.edge_set e ∈ G.edge_finset ↔ e ∈ G.edge_set := by { dunfold edge_finset, simp } -@[simp] lemma edge_set_univ_card [decidable_eq V] [fintype V] -[decidable_rel G.adj] : (univ : finset G.edge_set).card = G.edge_finset.card := +@[simp] lemma edge_set_univ_card [decidable_eq V] [fintype V] [decidable_rel G.adj] : + (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 From 2069d09a0d5843645b47fdf0b88f42a0509e7859 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 16:16:09 -0500 Subject: [PATCH 08/50] made changes --- src/combinatorics/simple_graph/basic.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index e1df5947e6990..304c548c168c3 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -161,10 +161,10 @@ fintype.card_of_subtype G.edge_finset (mem_edge_finset _) by tauto @[simp] lemma mem_incidence_set (v w : V) : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w := -by { dsimp [incidence_set], simp } +by { by simp [incidence_set] } -lemma neighbor_set_edge_prop {v w : V} (h : w ∈ G.neighbor_set v) : ⟦(v, w)⟧ ∈ G.incidence_set v := -by { rw mem_neighbor_set at h, simpa } +lemma mem_incidence_iff_neighbor {v w : V} : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ w ∈ G.neighbor_set v := +by simp only [mem_incidence_set, mem_neighbor_set] lemma adj_incidence_set_inter {v : V} {e : sym2 V} (he : e ∈ G.edge_set) (h : v ∈ e) : G.incidence_set v ∩ G.incidence_set h.other = {e} := @@ -191,8 +191,8 @@ by { cases h, rwa [←sym2.mem_other_spec' h_right, mem_edge_set] at h_left } @[simp] lemma incidence_other_neighbor_edge {v w : V} (h : w ∈ G.neighbor_set v) : - G.incidence_set_other (G.neighbor_set_edge_prop h) = w := -sym2.congr_right.mp (sym2.mem_other_spec' (G.neighbor_set_edge_prop h).right) + G.incidence_set_other (G.mem_incidence_iff_neighbor.mpr h) = w := +sym2.congr_right.mp (sym2.mem_other_spec' (G.mem_incidence_iff_neighbor.mpr h).right) /-- There is an equivalence between the set of edges incident to a given @@ -200,9 +200,9 @@ vertex and the set of vertices adjacent to the vertex. -/ @[simps] def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := { to_fun := λ e, ⟨G.incidence_set_other e.2, G.incidence_other_prop e.2⟩, - inv_fun := λ w, ⟨⟦(v, w.1)⟧, G.neighbor_set_edge_prop w.2⟩, - left_inv := by { intro x, dsimp [incidence_set_other], simp }, - right_inv := by { intro x, rcases x with ⟨w, hw⟩, simp, } } + inv_fun := λ w, ⟨⟦(v, w.1)⟧, G.mem_incidence_iff_neighbor.mpr w.2⟩, + left_inv := λ x, by simp [incidence_set_other], + right_inv := λ ⟨w, hw⟩, by simp } end incidence From 9896dc90426e49a76e5bb3c7cc58d9e5d6366f50 Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Wed, 2 Dec 2020 16:24:59 -0500 Subject: [PATCH 09/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Bryan Gin-ge Chen --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 304c548c168c3..6fd6ebe800c18 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -161,7 +161,7 @@ fintype.card_of_subtype G.edge_finset (mem_edge_finset _) by tauto @[simp] lemma mem_incidence_set (v w : V) : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w := -by { by simp [incidence_set] } +by { simp [incidence_set] } lemma mem_incidence_iff_neighbor {v w : V} : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ w ∈ G.neighbor_set v := by simp only [mem_incidence_set, mem_neighbor_set] From 2f5c5b3995836a07572ea8723e589643f79b28ee Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 18:18:38 -0500 Subject: [PATCH 10/50] fixed proof (thanks Kyle) --- src/combinatorics/simple_graph/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 6fd6ebe800c18..6c65c30e9bee7 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -65,8 +65,8 @@ symmetrizes the relation and makes it irreflexive. -/ def simple_graph_from_rel {V : Type u} (r : V → V → Prop) : simple_graph V := { adj := λ a b, (a ≠ b) ∧ (r a b ∨ r b a), - sym := by finish, - loopless := by finish } + sym := λ a b ⟨hn, hr⟩, ⟨ne.symm hn, or.symm hr⟩, + loopless := λ a ⟨hn, _⟩, hn rfl } @[simp] lemma simple_graph_from_rel_adj {V : Type u} (r : V → V → Prop) (v w : V) : From 47891ad113effbd6d6fddf923054ec7fec7bdd49 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Wed, 2 Dec 2020 18:28:52 -0500 Subject: [PATCH 11/50] oops --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 6c65c30e9bee7..c50a28b49f51f 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -107,7 +107,7 @@ The `incidence_set` is the set of edges incident to a given vertex. def incidence_set (v : V) : set (sym2 V) := {e ∈ G.edge_set | v ∈ e} lemma incidence_set_subset (v : V) : G.incidence_set v ⊆ G.edge_set := -by tidy +λ _ h, h.1 @[simp] lemma mem_edge_set {v w : V} : ⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w := From f08ca7912f159c059b6fe256cdef1b4e741630d8 Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Thu, 3 Dec 2020 00:50:21 -0500 Subject: [PATCH 12/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index c50a28b49f51f..2cf1034d1d4ad 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -183,7 +183,7 @@ variable [decidable_eq V] /-- Given an edge incident to a particular vertex, get the other vertex on the edge. -/ -def incidence_set_other {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' +def other_vertex_of_incident {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' lemma incidence_other_prop {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : G.incidence_set_other h ∈ G.neighbor_set v := From 175f9ddefa08187ee95ad0b61d65aa822b5eb64d Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Thu, 3 Dec 2020 01:15:29 -0500 Subject: [PATCH 13/50] changed lemma name --- src/combinatorics/simple_graph/basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index c50a28b49f51f..b3ef40c569742 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -183,15 +183,15 @@ variable [decidable_eq V] /-- Given an edge incident to a particular vertex, get the other vertex on the edge. -/ -def incidence_set_other {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' +def other_vertex_of_incident {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' lemma incidence_other_prop {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : -G.incidence_set_other h ∈ G.neighbor_set v := +G.other_vertex_of_incident h ∈ G.neighbor_set v := by { cases h, rwa [←sym2.mem_other_spec' h_right, mem_edge_set] at h_left } @[simp] lemma incidence_other_neighbor_edge {v w : V} (h : w ∈ G.neighbor_set v) : - G.incidence_set_other (G.mem_incidence_iff_neighbor.mpr h) = w := + G.other_vertex_of_incident (G.mem_incidence_iff_neighbor.mpr h) = w := sym2.congr_right.mp (sym2.mem_other_spec' (G.mem_incidence_iff_neighbor.mpr h).right) /-- @@ -199,9 +199,9 @@ There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex. -/ @[simps] def incidence_set_equiv_neighbor_set (v : V) : G.incidence_set v ≃ G.neighbor_set v := -{ to_fun := λ e, ⟨G.incidence_set_other e.2, G.incidence_other_prop e.2⟩, +{ to_fun := λ e, ⟨G.other_vertex_of_incident e.2, G.incidence_other_prop e.2⟩, inv_fun := λ w, ⟨⟦(v, w.1)⟧, G.mem_incidence_iff_neighbor.mpr w.2⟩, - left_inv := λ x, by simp [incidence_set_other], + left_inv := λ x, by simp [other_vertex_of_incident], right_inv := λ ⟨w, hw⟩, by simp } end incidence From 25e8bc97a21cece09ded077a4ff0f426ef1d76b3 Mon Sep 17 00:00:00 2001 From: Alena Gusakov Date: Thu, 3 Dec 2020 01:21:41 -0500 Subject: [PATCH 14/50] golfed proof --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index b3ef40c569742..145604687682f 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -258,7 +258,7 @@ by { rw fintype.card_congr (G.incidence_set_equiv_neighbor_set v), simp } @[simp] lemma mem_incidence_finset [decidable_eq V] (e : sym2 V) : e ∈ G.incidence_finset v ↔ e ∈ G.incidence_set v := -by { dunfold incidence_finset, simp } +set.mem_to_finset end finite_at From 80141b43259d673c6deff50cdc06263f2d338f3e Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:07:10 -0500 Subject: [PATCH 15/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Eric Wieser --- src/combinatorics/simple_graph/basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 145604687682f..599cc9200fa46 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -63,14 +63,14 @@ structure simple_graph (V : Type u) := Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive. -/ -def simple_graph_from_rel {V : Type u} (r : V → V → Prop) : simple_graph V := +def simple_graph.from_rel {V : Type u} (r : V → V → Prop) : simple_graph V := { adj := λ a b, (a ≠ b) ∧ (r a b ∨ r b a), sym := λ a b ⟨hn, hr⟩, ⟨ne.symm hn, or.symm hr⟩, loopless := λ a ⟨hn, _⟩, hn rfl } @[simp] -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) := +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) := by refl /-- From 4949f2c293972b37a7e11beb645e96fd44901710 Mon Sep 17 00:00:00 2001 From: agusakov <39916842+agusakov@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:07:23 -0500 Subject: [PATCH 16/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Eric Wieser --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 599cc9200fa46..a28184c3201d5 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -186,7 +186,7 @@ Given an edge incident to a particular vertex, get the other vertex on the edge. def other_vertex_of_incident {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' lemma incidence_other_prop {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : -G.other_vertex_of_incident h ∈ G.neighbor_set v := + G.other_vertex_of_incident h ∈ G.neighbor_set v := by { cases h, rwa [←sym2.mem_other_spec' h_right, mem_edge_set] at h_left } @[simp] From 218d8b3104557e5f185515652bd0ce285fb6dd44 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 05:19:43 -0800 Subject: [PATCH 17/50] Added the degree-sum formula for simple graphs and some sorry'd corollaries --- src/combinatorics/simple_graph/basic.lean | 10 + src/combinatorics/simple_graph/handshake.lean | 193 ++++++++++++++++++ src/data/sym2.lean | 9 + 3 files changed, 212 insertions(+) create mode 100644 src/combinatorics/simple_graph/handshake.lean diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 0447093965a81..68b4ee3686e1d 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -140,6 +140,12 @@ end instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] : fintype G.edge_set := by { dunfold edge_set, exact subtype.fintype _ } +instance mem_edges_decidable [decidable_eq V] [decidable_rel G.adj] (e : sym2 V) : + decidable (e ∈ G.edge_set) := by { dunfold edge_set, apply_instance } + +instance mem_incidence_set_decidable [decidable_eq V] [decidable_rel G.adj] (v : V) (e : sym2 V) : + decidable (e ∈ G.incidence_set v) := by { dsimp [incidence_set], apply_instance } + /-- The `edge_set` of the graph as a `finset`. -/ @@ -186,6 +192,10 @@ Given an edge incident to a particular vertex, get the other vertex on the edge. -/ def other_vertex_of_incident {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : V := h.2.other' +lemma edge_mem_other_incident_set {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : + e ∈ G.incidence_set (G.other_vertex_of_incident h) := +by { use h.1, simp [other_vertex_of_incident, sym2.mem_other_mem'] } + lemma incidence_other_prop {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) : G.other_vertex_of_incident h ∈ G.neighbor_set v := by { cases h, rwa [←sym2.mem_other_spec' h_right, mem_edge_set] at h_left } diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean new file mode 100644 index 0000000000000..6778747df223f --- /dev/null +++ b/src/combinatorics/simple_graph/handshake.lean @@ -0,0 +1,193 @@ +/- +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: Kyle Miller. +-/ +import combinatorics.simple_graph.basic +import algebra.big_operators.basic +/-! +# Degree-sum formula and handshaking lemma + +The degree-sum formula is that the sum of the degrees of a finite +graph is equal to twice the number of edges. The handshaking lemma is +a corollary, which is that the number of odd-degree vertices is even. + +## Main definitions + +- A `dart` is a directed edge, consisting of a vertex and an edge incident to it. +- `simple_graph.sum_degrees_eq_twice_card_edges` is the degree-sum formula. +- `simple_graph.card_odd_degree_vertices_is_even` is the handshaking lemma. +- `simple_graph.card_odd_degree_vertices_ne_is_odd` is that the number of odd-degree + vertices different from a given odd-degree vertex is odd. +- `simple_graph.exists_ne_odd_degree_if_exists_odd` is that the existence of an + odd-degree vertex implies the existence of another one. + +## Implementation notes + +We give a combinatorial proof by using the fact that the map from +darts to vertices has fibers whose cardinalities are the degrees and +that the map from darts to edges is 2-to-1. + +## Tags + +simple graphs, sums +-/ +open finset + +open_locale big_operators + +namespace simple_graph +universes u v +variables {V : Type u} (G : simple_graph V) + +/-- A `dart` is a directed edge, consisting of a vertex and an edge incident to it -/ +@[reducible] +def dart := Σ (v : V), G.incidence_set v + +/-- Gets the vertex at the start of the dart. -/ +def dart_vert : G.dart → V := sigma.fst + +/-- Gets the edge that the dart runs through. -/ +def dart_edge : G.dart → sym2 V := λ d, d.snd + +lemma dart_vert_mem (d : G.dart) : G.dart_vert d ∈ G.dart_edge d := +by { rcases d with ⟨v,e,he,hv⟩, simp [dart_vert, dart_edge, hv] } + +lemma dart_edge_mem (d : G.dart) : G.dart_edge d ∈ G.edge_set := +by { rcases d with ⟨v,e,he,hv⟩, exact he } + +lemma dart_edge_mem_incidence_set (d : G.dart) : G.dart_edge d ∈ G.incidence_set (G.dart_vert d) := +d.snd.property + +lemma dart.ext {d₁ d₂ : G.dart} + (hv : G.dart_vert d₁ = G.dart_vert d₂) (he : G.dart_edge d₁ = G.dart_edge d₂) : + d₁ = d₂ := +by { rcases d₁ with ⟨v₁, e₁, he₁, hv₁⟩, rcases d₂ with ⟨v₂, e₂, he₂, hv₂⟩, + dsimp only [dart_vert, dart_edge, subtype.coe_mk] at hv he, subst v₂, subst e₂, } + +lemma dart.ext_iff (d₁ d₂ : G.dart) : + d₁ = d₂ ↔ G.dart_vert d₁ = G.dart_vert d₂ ∧ G.dart_edge d₁ = G.dart_edge d₂ := +by { split, rintro rfl, tauto, rintro ⟨hv, he⟩, apply dart.ext G hv he } + +def dart_rev [decidable_eq V] (d : G.dart) : G.dart := +⟨sym2.mem.other' (G.dart_vert_mem d), G.dart_edge d, G.edge_mem_other_incident_set d.snd.property⟩ + +@[simp] +lemma dart_edge_of_dart_rev [decidable_eq V] (d : G.dart) : + G.dart_edge (G.dart_rev d) = G.dart_edge d := rfl + +lemma dart_rev_invol [decidable_eq V] (d : G.dart) : G.dart_rev (G.dart_rev d) = d := +begin + apply dart.ext, + apply sym2.other_invol', + rcases d with ⟨v, e, he, hv⟩, + simp [dart_edge, dart_rev], +end + +lemma dart_rev_no_fixedpoints [decidable_eq V] (d : G.dart) : d ≠ G.dart_rev d := +begin + intro h, rw dart.ext_iff at h, + dsimp [dart_vert, dart_rev] at h, + apply G.edge_other_ne (G.dart_edge_mem d) (G.dart_vert_mem d), + convert h.1.symm, rw sym2.other_eq_other', +end + +lemma dart_edge_eq_iff [decidable_eq V] (d₁ d₂ : G.dart) : + G.dart_edge d₁ = G.dart_edge d₂ ↔ d₁ = d₂ ∨ d₁ = G.dart_rev d₂ := +begin + split, + { rw [dart.ext_iff, dart.ext_iff], + rcases d₁ with ⟨v₁, e₁, he₁, hv₁⟩, + rcases d₂ with ⟨v₂, e₂, he₂, hv₂⟩, + dsimp [dart_edge, dart_vert, dart_rev], + rintro rfl, simp only [and_true, eq_self_iff_true], + by_cases hveq : v₁ = v₂, + { left, subst hveq, }, + { right, + have he : e₁ = ⟦(v₁, v₂)⟧ := (sym2.elems_iff_eq hveq).mp ⟨hv₁, hv₂⟩, + subst e₁, + have h' := sym2.mem_other_spec' hv₂, + rw [sym2.eq_swap, sym2.congr_left] at h', + convert h'.symm, }, }, + { intro h, cases h; subst d₁, refl, }, +end + +def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := λ ee, ⟨v, ee⟩ + +lemma dart_from_incidence_set_inj (v : V) : function.injective (G.dart_from_incidence_set v) := +by { dsimp only [dart_from_incidence_set], exact sigma_mk_injective } + +variables [fintype V] [decidable_eq V] [decidable_rel G.adj] + +lemma dart_vert_fiber_card_eq_degree (v : V) : + (univ.filter (λ d, G.dart_vert d = v)).card = G.degree v := +begin + have hh := card_image_of_injective univ (G.dart_from_incidence_set_inj v), + rw [finset.card_univ, card_incidence_set_eq_degree] at hh, + convert hh, + ext d, simp, + split, + { rintro rfl, use G.dart_edge d, use G.dart_edge_mem_incidence_set d, + apply dart.ext; simp [dart_from_incidence_set, dart_vert, dart_edge], }, + { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart_vert] }, +end + +lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := +begin + convert_to (univ : finset G.dart).card = _, + rw @card_eq_sum_card_fiberwise _ _ _ G.dart_vert _ univ (λ d h, mem_univ _), + simp [G.dart_vert_fiber_card_eq_degree], +end + +lemma dart_edge_fiber_card_eq_2 (e : sym2 V) (h : e ∈ G.edge_set) : + (filter (λ (d : G.dart), G.dart_edge d = e) univ).card = 2 := +begin + refine quotient.ind (λ p h, _) e h, cases p with v w, + let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, + convert_to _ = finset.card {d, G.dart_rev d}, + { rw [card_insert_of_not_mem, card_singleton], simp [G.dart_rev_no_fixedpoints d], }, + congr, ext d', + simp only [true_and, mem_filter, mem_insert, mem_univ, mem_singleton], + exact G.dart_edge_eq_iff d' d, +end + +lemma dart_card_eq_twice_card_edges : fintype.card G.dart = 2 * G.edge_finset.card := +begin + convert_to (univ : finset G.dart).card = _, + rw @card_eq_sum_card_fiberwise _ _ _ G.dart_edge _ G.edge_finset + (λ d h, by { rw mem_edge_finset, apply G.dart_edge_mem }), + rw @sum_congr _ _ G.edge_finset G.edge_finset + (λ e, (univ.filter (λ (x : G.dart), G.dart_edge x = e)).card) (λ e, 2) _ rfl, + simp [mul_comm], + intros e h, rw mem_edge_finset at h, + exact G.dart_edge_fiber_card_eq_2 e h, +end + +/-- The degree-sum formula. -/ +theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * G.edge_finset.card := +G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges + +/- TODO nat.odd and nat.even used to be decidable predicates -- where did those go? -/ +instance odd_decidable (n : ℕ) : decidable (odd n) := +begin + sorry +end + +theorem card_odd_degree_vertices_is_even : even (univ.filter (λ v, odd (G.degree v))).card := +begin + sorry +end + +theorem card_odd_degree_vertices_ne_is_odd (v : V) (h : odd (G.degree v)) : + odd (univ.filter (λ w, w ≠ v ∧ odd (G.degree w))).card := +begin + sorry +end + +theorem exists_ne_odd_degree_if_exists_odd (v : V) (h : odd (G.degree v)) : + ∃ (w : V), w ≠ v ∧ odd (G.degree w) := +begin + sorry +end + +end simple_graph diff --git a/src/data/sym2.lean b/src/data/sym2.lean index 4cdc4b912aad4..d73106a9ce9b5 100644 --- a/src/data/sym2.lean +++ b/src/data/sym2.lean @@ -173,6 +173,15 @@ begin cases hx; subst x; cases hy; subst y; cases hx'; try { subst x' }; cases hy'; try { subst y' }; cc, end +instance mem.decidable [decidable_eq α] (x : α) (z : sym2 α) : decidable (x ∈ z) := +begin + refine quotient.rec_on_subsingleton z (λ w, _), + cases w with y₁ y₂, + by_cases h₁ : x = y₁, subst x, exact is_true (mk_has_mem _ _), + by_cases h₂ : x = y₂, subst x, exact is_true (mk_has_mem_right _ _), + apply is_false, intro h, rw mem_iff at h, cases h, exact h₁ h, exact h₂ h, +end + end membership /-- From a2dd0c73d096adfde65464a6296d5164102eb8c1 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 05:36:06 -0800 Subject: [PATCH 18/50] exposed combinatorics a bit more --- src/combinatorics/simple_graph/handshake.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 6778747df223f..bd1bf33e2b0d1 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -139,16 +139,22 @@ begin simp [G.dart_vert_fiber_card_eq_degree], end +lemma dart_edge_fiber (d : G.dart) : + (univ.filter (λ (d' : G.dart), G.dart_edge d' = G.dart_edge d)) = {d, G.dart_rev d} := +begin + ext d', + simp only [true_and, mem_filter, mem_insert, mem_univ, mem_singleton], + exact G.dart_edge_eq_iff d' d, +end + lemma dart_edge_fiber_card_eq_2 (e : sym2 V) (h : e ∈ G.edge_set) : - (filter (λ (d : G.dart), G.dart_edge d = e) univ).card = 2 := + (univ.filter (λ (d : G.dart), G.dart_edge d = e)).card = 2 := begin refine quotient.ind (λ p h, _) e h, cases p with v w, let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, convert_to _ = finset.card {d, G.dart_rev d}, { rw [card_insert_of_not_mem, card_singleton], simp [G.dart_rev_no_fixedpoints d], }, - congr, ext d', - simp only [true_and, mem_filter, mem_insert, mem_univ, mem_singleton], - exact G.dart_edge_eq_iff d' d, + congr, apply G.dart_edge_fiber d, end lemma dart_card_eq_twice_card_edges : fintype.card G.dart = 2 * G.edge_finset.card := From f62c0301166ebefee7f1d293f9faf08843aa920d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 05:40:14 -0800 Subject: [PATCH 19/50] nonterminal simp --- src/combinatorics/simple_graph/handshake.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index bd1bf33e2b0d1..68da3f939ce49 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -125,7 +125,8 @@ begin have hh := card_image_of_injective univ (G.dart_from_incidence_set_inj v), rw [finset.card_univ, card_incidence_set_eq_degree] at hh, convert hh, - ext d, simp, + ext d, + simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, { rintro rfl, use G.dart_edge d, use G.dart_edge_mem_incidence_set d, apply dart.ext; simp [dart_from_incidence_set, dart_vert, dart_edge], }, From f63f1e615d6f938e228ac2c7c38d072814d3eb99 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 13:54:43 -0800 Subject: [PATCH 20/50] linter (except for some unused arguments that will be used later) --- src/combinatorics/simple_graph/basic.lean | 2 +- src/combinatorics/simple_graph/handshake.lean | 14 +++++++++++--- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index bdc88f7a9c1d5..8085cf35a2b25 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -140,7 +140,7 @@ end instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] : fintype G.edge_set := by { dunfold edge_set, exact subtype.fintype _ } -instance mem_edges_decidable [decidable_eq V] [decidable_rel G.adj] (e : sym2 V) : +instance mem_edges_decidable [decidable_rel G.adj] (e : sym2 V) : decidable (e ∈ G.edge_set) := by { dunfold edge_set, apply_instance } instance mem_incidence_set_decidable [decidable_eq V] [decidable_rel G.adj] (v : V) (e : sym2 V) : diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 68da3f939ce49..e1aad9c0b464f 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -69,6 +69,7 @@ lemma dart.ext_iff (d₁ d₂ : G.dart) : d₁ = d₂ ↔ G.dart_vert d₁ = G.dart_vert d₂ ∧ G.dart_edge d₁ = G.dart_edge d₂ := by { split, rintro rfl, tauto, rintro ⟨hv, he⟩, apply dart.ext G hv he } +/-- Reverses the orientation of a dart. -/ def dart_rev [decidable_eq V] (d : G.dart) : G.dart := ⟨sym2.mem.other' (G.dart_vert_mem d), G.dart_edge d, G.edge_mem_other_incident_set d.snd.property⟩ @@ -112,11 +113,13 @@ begin { intro h, cases h; subst d₁, refl, }, end +/-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := λ ee, ⟨v, ee⟩ lemma dart_from_incidence_set_inj (v : V) : function.injective (G.dart_from_incidence_set v) := by { dsimp only [dart_from_incidence_set], exact sigma_mk_injective } +section degree_sum variables [fintype V] [decidable_eq V] [decidable_rel G.adj] lemma dart_vert_fiber_card_eq_degree (v : V) : @@ -174,27 +177,32 @@ end theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * G.edge_finset.card := G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges +end degree_sum + /- TODO nat.odd and nat.even used to be decidable predicates -- where did those go? -/ instance odd_decidable (n : ℕ) : decidable (odd n) := begin sorry end -theorem card_odd_degree_vertices_is_even : even (univ.filter (λ v, odd (G.degree v))).card := +theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin sorry end -theorem card_odd_degree_vertices_ne_is_odd (v : V) (h : odd (G.degree v)) : +lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] + (v : V) (h : odd (G.degree v)) : odd (univ.filter (λ w, w ≠ v ∧ odd (G.degree w))).card := begin sorry end -theorem exists_ne_odd_degree_if_exists_odd (v : V) (h : odd (G.degree v)) : +lemma exists_ne_odd_degree_if_exists_odd [fintype V] + (v : V) (h : odd (G.degree v)) : ∃ (w : V), w ≠ v ∧ odd (G.degree w) := begin sorry end end simple_graph + From 0ef82ff09c6c2ddf2665b504d09542bbe55c6fb5 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 14:34:58 -0800 Subject: [PATCH 21/50] filled in some sorries, but still need the handshake lemma itself --- src/combinatorics/simple_graph/handshake.lean | 26 ++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index e1aad9c0b464f..6b7e4f691ea40 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -5,6 +5,7 @@ Author: Kyle Miller. -/ import combinatorics.simple_graph.basic import algebra.big_operators.basic +import tactic.omega /-! # Degree-sum formula and handshaking lemma @@ -187,6 +188,8 @@ end theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin + classical, + have h := G.sum_degrees_eq_twice_card_edges, sorry end @@ -194,15 +197,32 @@ lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] (v : V) (h : odd (G.degree v)) : odd (univ.filter (λ w, w ≠ v ∧ odd (G.degree w))).card := begin - sorry + rcases G.card_odd_degree_vertices_is_even with ⟨k, hg⟩, + have hk : 0 < k, + { have hh : (filter (λ (v : V), odd (G.degree v)) univ).nonempty, + { use v, simp only [true_and, mem_filter, mem_univ], use h, }, + rw ←card_pos at hh, rw hg at hh, clear hg, linarith, }, + have hc : (λ (w : V), w ≠ v ∧ odd (G.degree w)) = (λ (w : V), odd (G.degree w) ∧ w ≠ v), + { ext w, rw and_comm, }, + simp only [hc, filter_congr_decidable], + rw [←filter_filter, filter_ne'], + rw card_erase_of_mem, + use k - 1, rw nat.pred_eq_succ_iff, rw hg, clear hc hg, rw nat.mul_sub_left_distrib, omega, + simp only [true_and, mem_filter, mem_univ], + exact h, end lemma exists_ne_odd_degree_if_exists_odd [fintype V] (v : V) (h : odd (G.degree v)) : ∃ (w : V), w ≠ v ∧ odd (G.degree w) := begin - sorry + haveI : decidable_eq V := by { classical, apply_instance }, + rcases G.card_odd_degree_vertices_ne_is_odd v h with ⟨k, hg⟩, + have hg' : (filter (λ (w : V), w ≠ v ∧ odd (G.degree w)) univ).card > 0, + { rw hg, apply nat.succ_pos, }, + rcases card_pos.mp hg' with ⟨w, hw⟩, + simp only [true_and, mem_filter, mem_univ, ne.def] at hw, + exact ⟨w, hw⟩, end end simple_graph - From 2ce46d9381f68ab48729e52a8926300c0d34750e Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 15:51:16 -0800 Subject: [PATCH 22/50] found data.nat.parity which has the necessary decidable instances --- src/combinatorics/simple_graph/handshake.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 6b7e4f691ea40..07e4aaf2a3486 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -5,6 +5,7 @@ Author: Kyle Miller. -/ import combinatorics.simple_graph.basic import algebra.big_operators.basic +import data.nat.parity import tactic.omega /-! # Degree-sum formula and handshaking lemma @@ -180,16 +181,12 @@ G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges end degree_sum -/- TODO nat.odd and nat.even used to be decidable predicates -- where did those go? -/ -instance odd_decidable (n : ℕ) : decidable (odd n) := -begin - sorry -end - -theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := +theorem card_odd_degree_vertices_is_even [fintype V] : + even (univ.filter (λ v, odd (G.degree v))).card := begin classical, - have h := G.sum_degrees_eq_twice_card_edges, + have h := congr_arg (% 2) G.sum_degrees_eq_twice_card_edges, + simp at h, sorry end From 39d98771991987811afc2dd1f68129170621a568 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 17:06:50 -0800 Subject: [PATCH 23/50] Filled in proofs, but still have a sorry in a zmod lemma --- src/combinatorics/simple_graph/handshake.lean | 45 +++++++++++++++++-- 1 file changed, 42 insertions(+), 3 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 07e4aaf2a3486..f652e9c70af6f 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -6,7 +6,9 @@ Author: Kyle Miller. import combinatorics.simple_graph.basic import algebra.big_operators.basic import data.nat.parity +import data.zmod.basic import tactic.omega +import tactic.fin_cases /-! # Degree-sum formula and handshaking lemma @@ -181,13 +183,50 @@ G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges end degree_sum +lemma zmod_cast_mod (a b : ℕ) : a % 2 = b % 2 ↔ (a : zmod 2) = (b : zmod 2) := +begin + sorry +end + +lemma zmod_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := +begin + rw nat.even_iff, + change _ ↔ n % 2 = 0 % 2, + rw zmod_cast_mod, + norm_num, +end + +lemma zmod_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := +begin + rw nat.odd_iff, + change _ ↔ n % 2 = 1 % 2, + rw zmod_cast_mod, + norm_num, +end + +lemma zmod_odd' (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := +begin + rw ←zmod_odd, + generalize h : (n : zmod 2) = m, + fin_cases m, simp, split, intro, refl, intros h, + let z : zmod 2 := ⟨0, _⟩, convert_to ¬_ = z, norm_num, +end + theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin classical, - have h := congr_arg (% 2) G.sum_degrees_eq_twice_card_edges, - simp at h, - sorry + have h := congr_arg ((λ n, ↑n) : ℕ → zmod 2) G.sum_degrees_eq_twice_card_edges, + simp only [zmod.cast_self, zero_mul, nat.cast_mul] at h, + rw sum_nat_cast at h, + rw ←sum_filter_ne_zero at h, + rw @sum_congr _ (zmod 2) _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h, + simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, + rw ←zmod_even, + convert h, + ext v, rw ←zmod_odd', split, intro h, convert h, intro h, convert h, + intros v, simp, + rw [zmod_even, zmod_odd, nat.odd_iff_not_even, imp_self], trivial, end lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] From 4ac35418aa9ddab760f39e15a0aa9913c88788dd Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 17:20:37 -0800 Subject: [PATCH 24/50] simplified these zmod proofs, but still missing key lemma --- src/combinatorics/simple_graph/handshake.lean | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index f652e9c70af6f..68cb21cc3dc06 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -188,7 +188,7 @@ begin sorry end -lemma zmod_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := +lemma zmod_eq_zero_iff_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := begin rw nat.even_iff, change _ ↔ n % 2 = 0 % 2, @@ -196,7 +196,7 @@ begin norm_num, end -lemma zmod_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := +lemma zmod_eq_one_iff_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := begin rw nat.odd_iff, change _ ↔ n % 2 = 1 % 2, @@ -204,13 +204,8 @@ begin norm_num, end -lemma zmod_odd' (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := -begin - rw ←zmod_odd, - generalize h : (n : zmod 2) = m, - fin_cases m, simp, split, intro, refl, intros h, - let z : zmod 2 := ⟨0, _⟩, convert_to ¬_ = z, norm_num, -end +lemma zmod_neq_zero_iff_odd (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := +by split; { contrapose, simp [zmod_eq_zero_iff_even], } theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := @@ -222,11 +217,11 @@ begin rw ←sum_filter_ne_zero at h, rw @sum_congr _ (zmod 2) _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h, simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, - rw ←zmod_even, + rw ←zmod_eq_zero_iff_even, convert h, - ext v, rw ←zmod_odd', split, intro h, convert h, intro h, convert h, + ext v, rw ←zmod_neq_zero_iff_odd, split, intro h, convert h, intro h, convert h, intros v, simp, - rw [zmod_even, zmod_odd, nat.odd_iff_not_even, imp_self], trivial, + rw [zmod_eq_zero_iff_even, zmod_eq_one_iff_odd, nat.odd_iff_not_even, imp_self], trivial, end lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] From d374ca0229185187c2494f20b880a7abbbee7672 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 17:30:33 -0800 Subject: [PATCH 25/50] found a way to prove the zmod lemmas, now it's complete --- src/combinatorics/simple_graph/handshake.lean | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 68cb21cc3dc06..515736c6eb8a0 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -183,30 +183,30 @@ G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges end degree_sum -lemma zmod_cast_mod (a b : ℕ) : a % 2 = b % 2 ↔ (a : zmod 2) = (b : zmod 2) := -begin - sorry -end + +section TODO_move lemma zmod_eq_zero_iff_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := begin + change (n : zmod 2) = ((0 : ℕ) : zmod 2) ↔ _, + rw zmod.eq_iff_modeq_nat, rw nat.even_iff, - change _ ↔ n % 2 = 0 % 2, - rw zmod_cast_mod, - norm_num, + trivial, end lemma zmod_eq_one_iff_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := begin + change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, + rw zmod.eq_iff_modeq_nat, rw nat.odd_iff, - change _ ↔ n % 2 = 1 % 2, - rw zmod_cast_mod, - norm_num, + trivial, end lemma zmod_neq_zero_iff_odd (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := by split; { contrapose, simp [zmod_eq_zero_iff_even], } +end TODO_move + theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin @@ -220,7 +220,7 @@ begin rw ←zmod_eq_zero_iff_even, convert h, ext v, rw ←zmod_neq_zero_iff_odd, split, intro h, convert h, intro h, convert h, - intros v, simp, + intros v, simp only [true_and, mem_filter, mem_univ, ne.def], rw [zmod_eq_zero_iff_even, zmod_eq_one_iff_odd, nat.odd_iff_not_even, imp_self], trivial, end From f8e7f435f2f9d5852c638252d435217b8c7f7630 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 17:42:19 -0800 Subject: [PATCH 26/50] fixed copyright line (had copied from basic.lean) --- src/combinatorics/simple_graph/handshake.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 515736c6eb8a0..2f326598d839a 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2020 Aaron Anderson, Jalex Stark, Kyle Miller. All rights reserved. +Copyright (c) 2020 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Kyle Miller. -/ From f9e11c0cbe863e19e47472becce955aee0cbe208 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 6 Dec 2020 23:09:34 -0800 Subject: [PATCH 27/50] b-mehta review --- src/combinatorics/simple_graph/handshake.lean | 26 ++++++++++++------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 2f326598d839a..eb661b30d4df2 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -34,7 +34,7 @@ that the map from darts to edges is 2-to-1. ## Tags -simple graphs, sums +simple graphs, sums, degree-sum formula, handshaking lemma -/ open finset @@ -45,14 +45,19 @@ universes u v variables {V : Type u} (G : simple_graph V) /-- A `dart` is a directed edge, consisting of a vertex and an edge incident to it -/ -@[reducible] def dart := Σ (v : V), G.incidence_set v +instance dart.fintype [fintype V] [decidable_eq V] [decidable_rel G.adj] : fintype (dart G) := +by { dunfold dart, apply_instance } + +instance dart.inhabited [inhabited V] [inhabited (G.incidence_set (default _))] : + inhabited G.dart := ⟨⟨default _, default _⟩⟩ + /-- Gets the vertex at the start of the dart. -/ def dart_vert : G.dart → V := sigma.fst /-- Gets the edge that the dart runs through. -/ -def dart_edge : G.dart → sym2 V := λ d, d.snd +def dart_edge : G.dart → sym2 V := λ d, (d.snd : sym2 V) lemma dart_vert_mem (d : G.dart) : G.dart_vert d ∈ G.dart_edge d := by { rcases d with ⟨v,e,he,hv⟩, simp [dart_vert, dart_edge, hv] } @@ -63,6 +68,7 @@ by { rcases d with ⟨v,e,he,hv⟩, exact he } lemma dart_edge_mem_incidence_set (d : G.dart) : G.dart_edge d ∈ G.incidence_set (G.dart_vert d) := d.snd.property +@[ext] lemma dart.ext {d₁ d₂ : G.dart} (hv : G.dart_vert d₁ = G.dart_vert d₂) (he : G.dart_edge d₁ = G.dart_edge d₂) : d₁ = d₂ := @@ -155,7 +161,7 @@ begin exact G.dart_edge_eq_iff d' d, end -lemma dart_edge_fiber_card_eq_2 (e : sym2 V) (h : e ∈ G.edge_set) : +lemma dart_edge_fiber_card (e : sym2 V) (h : e ∈ G.edge_set) : (univ.filter (λ (d : G.dart), G.dart_edge d = e)).card = 2 := begin refine quotient.ind (λ p h, _) e h, cases p with v w, @@ -174,10 +180,11 @@ begin (λ e, (univ.filter (λ (x : G.dart), G.dart_edge x = e)).card) (λ e, 2) _ rfl, simp [mul_comm], intros e h, rw mem_edge_finset at h, - exact G.dart_edge_fiber_card_eq_2 e h, + exact G.dart_edge_fiber_card e h, end -/-- The degree-sum formula. -/ +/-- The degree-sum formula. This is also known as the handshaking lemma, which might +more specifically refer to `simple_graph.card_odd_degree_vertices_is_even`. -/ theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * G.edge_finset.card := G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges @@ -189,16 +196,14 @@ section TODO_move lemma zmod_eq_zero_iff_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := begin change (n : zmod 2) = ((0 : ℕ) : zmod 2) ↔ _, - rw zmod.eq_iff_modeq_nat, - rw nat.even_iff, + rw [zmod.eq_iff_modeq_nat, nat.even_iff], trivial, end lemma zmod_eq_one_iff_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := begin change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, - rw zmod.eq_iff_modeq_nat, - rw nat.odd_iff, + rw [zmod.eq_iff_modeq_nat, nat.odd_iff], trivial, end @@ -207,6 +212,7 @@ by split; { contrapose, simp [zmod_eq_zero_iff_even], } end TODO_move +/-- The handshaking lemma. See also `simple_graph.sum_degrees_eq_twice_card_edges`. -/ theorem card_odd_degree_vertices_is_even [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin From 5968b385edc0b34511b008f0d04923be47ed7576 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 00:53:46 -0800 Subject: [PATCH 28/50] switched from sigma type to structure, removing boilerplate and adding clarity --- src/combinatorics/simple_graph/handshake.lean | 126 ++++++++---------- 1 file changed, 57 insertions(+), 69 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index eb661b30d4df2..aad710f5b2a32 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -8,7 +8,6 @@ import algebra.big_operators.basic import data.nat.parity import data.zmod.basic import tactic.omega -import tactic.fin_cases /-! # Degree-sum formula and handshaking lemma @@ -45,95 +44,84 @@ universes u v variables {V : Type u} (G : simple_graph V) /-- A `dart` is a directed edge, consisting of a vertex and an edge incident to it -/ -def dart := Σ (v : V), G.incidence_set v +@[ext, derive decidable_eq] +structure dart := +(vert : V) +(edge : sym2 V) +(edge_mem : edge ∈ G.edge_set) +(vert_mem : vert ∈ edge) + +def dart_equiv_sigma : G.dart ≃ Σ v, G.incidence_set v := +{ to_fun := λ d, ⟨d.vert, d.edge, d.edge_mem, d.vert_mem⟩, + inv_fun := λ s, ⟨s.fst, s.snd, s.snd.property.1, s.snd.property.2⟩, + left_inv := λ d, by { ext, simp only, simp only [subtype.coe_mk], }, + right_inv := λ s, by { ext, simp only, simp only [subtype.coe_eta], } } instance dart.fintype [fintype V] [decidable_eq V] [decidable_rel G.adj] : fintype (dart G) := -by { dunfold dart, apply_instance } +fintype.of_equiv _ G.dart_equiv_sigma.symm instance dart.inhabited [inhabited V] [inhabited (G.incidence_set (default _))] : - inhabited G.dart := ⟨⟨default _, default _⟩⟩ + inhabited G.dart := ⟨G.dart_equiv_sigma.symm ⟨default _, default _⟩⟩ -/-- Gets the vertex at the start of the dart. -/ -def dart_vert : G.dart → V := sigma.fst +variables {G} -/-- Gets the edge that the dart runs through. -/ -def dart_edge : G.dart → sym2 V := λ d, (d.snd : sym2 V) - -lemma dart_vert_mem (d : G.dart) : G.dart_vert d ∈ G.dart_edge d := -by { rcases d with ⟨v,e,he,hv⟩, simp [dart_vert, dart_edge, hv] } - -lemma dart_edge_mem (d : G.dart) : G.dart_edge d ∈ G.edge_set := -by { rcases d with ⟨v,e,he,hv⟩, exact he } - -lemma dart_edge_mem_incidence_set (d : G.dart) : G.dart_edge d ∈ G.incidence_set (G.dart_vert d) := -d.snd.property - -@[ext] -lemma dart.ext {d₁ d₂ : G.dart} - (hv : G.dart_vert d₁ = G.dart_vert d₂) (he : G.dart_edge d₁ = G.dart_edge d₂) : - d₁ = d₂ := -by { rcases d₁ with ⟨v₁, e₁, he₁, hv₁⟩, rcases d₂ with ⟨v₂, e₂, he₂, hv₂⟩, - dsimp only [dart_vert, dart_edge, subtype.coe_mk] at hv he, subst v₂, subst e₂, } - -lemma dart.ext_iff (d₁ d₂ : G.dart) : - d₁ = d₂ ↔ G.dart_vert d₁ = G.dart_vert d₂ ∧ G.dart_edge d₁ = G.dart_edge d₂ := -by { split, rintro rfl, tauto, rintro ⟨hv, he⟩, apply dart.ext G hv he } +lemma dart.edge_mem_incidence_set (d : G.dart) : d.edge ∈ G.incidence_set d.vert := +⟨d.edge_mem, d.vert_mem⟩ /-- Reverses the orientation of a dart. -/ -def dart_rev [decidable_eq V] (d : G.dart) : G.dart := -⟨sym2.mem.other' (G.dart_vert_mem d), G.dart_edge d, G.edge_mem_other_incident_set d.snd.property⟩ +def dart.rev [decidable_eq V] (d : G.dart) : G.dart := +{ vert := sym2.mem.other' d.vert_mem, + edge := d.edge, + edge_mem := d.edge_mem, + vert_mem := sym2.mem_other_mem' d.vert_mem } -@[simp] -lemma dart_edge_of_dart_rev [decidable_eq V] (d : G.dart) : - G.dart_edge (G.dart_rev d) = G.dart_edge d := rfl +@[simp] lemma dart_edge_of_dart_rev [decidable_eq V] (d : G.dart) : d.rev.edge = d.edge := rfl -lemma dart_rev_invol [decidable_eq V] (d : G.dart) : G.dart_rev (G.dart_rev d) = d := +lemma dart_rev_invol [decidable_eq V] (d : G.dart) : d.rev.rev = d := begin apply dart.ext, apply sym2.other_invol', - rcases d with ⟨v, e, he, hv⟩, - simp [dart_edge, dart_rev], + simp only [dart_edge_of_dart_rev], end -lemma dart_rev_no_fixedpoints [decidable_eq V] (d : G.dart) : d ≠ G.dart_rev d := +lemma dart_rev_no_fixedpoints [decidable_eq V] (d : G.dart) : d ≠ d.rev := begin intro h, rw dart.ext_iff at h, - dsimp [dart_vert, dart_rev] at h, - apply G.edge_other_ne (G.dart_edge_mem d) (G.dart_vert_mem d), + dsimp [dart.vert, dart.rev] at h, + apply G.edge_other_ne d.edge_mem d.vert_mem, convert h.1.symm, rw sym2.other_eq_other', end lemma dart_edge_eq_iff [decidable_eq V] (d₁ d₂ : G.dart) : - G.dart_edge d₁ = G.dart_edge d₂ ↔ d₁ = d₂ ∨ d₁ = G.dart_rev d₂ := + d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.rev := begin + have h₁ : d₁.edge = ⟦(d₁.vert, d₁.rev.vert)⟧ := (sym2.mem_other_spec' d₁.vert_mem).symm, + have h₂ : d₂.edge = ⟦(d₂.vert, d₂.rev.vert)⟧ := (sym2.mem_other_spec' d₂.vert_mem).symm, split, - { rw [dart.ext_iff, dart.ext_iff], - rcases d₁ with ⟨v₁, e₁, he₁, hv₁⟩, - rcases d₂ with ⟨v₂, e₂, he₂, hv₂⟩, - dsimp [dart_edge, dart_vert, dart_rev], - rintro rfl, simp only [and_true, eq_self_iff_true], - by_cases hveq : v₁ = v₂, - { left, subst hveq, }, - { right, - have he : e₁ = ⟦(v₁, v₂)⟧ := (sym2.elems_iff_eq hveq).mp ⟨hv₁, hv₂⟩, - subst e₁, - have h' := sym2.mem_other_spec' hv₂, - rw [sym2.eq_swap, sym2.congr_left] at h', - convert h'.symm, }, }, + { rw [dart.ext_iff, dart.ext_iff, dart_edge_of_dart_rev], + intro h, simp only [h, and_true, eq_self_iff_true], + rw [h₁, h₂, sym2.eq_iff] at h, + cases h, + { exact or.inl h.1 }, + { exact or.inr h.1 }, }, { intro h, cases h; subst d₁, refl, }, end +variables (G) + /-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ -def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := λ ee, ⟨v, ee⟩ +def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := +λ ee, ⟨v, ee, ee.property.1, ee.property.2⟩ lemma dart_from_incidence_set_inj (v : V) : function.injective (G.dart_from_incidence_set v) := -by { dsimp only [dart_from_incidence_set], exact sigma_mk_injective } +by { intros e₁ e₂, dsimp only [dart_from_incidence_set, dart_equiv_sigma], + simp only [true_and, equiv.coe_fn_symm_mk, eq_self_iff_true], exact subtype.ext, } section degree_sum variables [fintype V] [decidable_eq V] [decidable_rel G.adj] lemma dart_vert_fiber_card_eq_degree (v : V) : - (univ.filter (λ d, G.dart_vert d = v)).card = G.degree v := + (univ.filter (λ d : G.dart, d.vert = v)).card = G.degree v := begin have hh := card_image_of_injective univ (G.dart_from_incidence_set_inj v), rw [finset.card_univ, card_incidence_set_eq_degree] at hh, @@ -141,43 +129,43 @@ begin ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, - { rintro rfl, use G.dart_edge d, use G.dart_edge_mem_incidence_set d, - apply dart.ext; simp [dart_from_incidence_set, dart_vert, dart_edge], }, - { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart_vert] }, + { rintro rfl, use d.edge, use d.edge_mem_incidence_set, + apply dart.ext; simp [dart_from_incidence_set, dart.vert, dart.edge], }, + { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart.vert] }, end -lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := +lemma dart_card_eq_sum_degrees [hd : decidable_eq V] : fintype.card G.dart = ∑ v, G.degree v := begin convert_to (univ : finset G.dart).card = _, - rw @card_eq_sum_card_fiberwise _ _ _ G.dart_vert _ univ (λ d h, mem_univ _), + rw @card_eq_sum_card_fiberwise _ _ hd dart.vert _ univ (λ d h, mem_univ _), simp [G.dart_vert_fiber_card_eq_degree], end lemma dart_edge_fiber (d : G.dart) : - (univ.filter (λ (d' : G.dart), G.dart_edge d' = G.dart_edge d)) = {d, G.dart_rev d} := + (univ.filter (λ (d' : G.dart), d'.edge = d.edge)) = {d, d.rev} := begin ext d', simp only [true_and, mem_filter, mem_insert, mem_univ, mem_singleton], - exact G.dart_edge_eq_iff d' d, + exact dart_edge_eq_iff d' d, end lemma dart_edge_fiber_card (e : sym2 V) (h : e ∈ G.edge_set) : - (univ.filter (λ (d : G.dart), G.dart_edge d = e)).card = 2 := + (univ.filter (λ (d : G.dart), d.edge = e)).card = 2 := begin refine quotient.ind (λ p h, _) e h, cases p with v w, let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, - convert_to _ = finset.card {d, G.dart_rev d}, - { rw [card_insert_of_not_mem, card_singleton], simp [G.dart_rev_no_fixedpoints d], }, + convert_to _ = finset.card {d, d.rev}, + { rw [card_insert_of_not_mem, card_singleton], simp [dart_rev_no_fixedpoints d], }, congr, apply G.dart_edge_fiber d, end lemma dart_card_eq_twice_card_edges : fintype.card G.dart = 2 * G.edge_finset.card := begin convert_to (univ : finset G.dart).card = _, - rw @card_eq_sum_card_fiberwise _ _ _ G.dart_edge _ G.edge_finset - (λ d h, by { rw mem_edge_finset, apply G.dart_edge_mem }), + rw @card_eq_sum_card_fiberwise _ _ _ dart.edge _ G.edge_finset + (λ d h, by { rw mem_edge_finset, apply dart.edge_mem }), rw @sum_congr _ _ G.edge_finset G.edge_finset - (λ e, (univ.filter (λ (x : G.dart), G.dart_edge x = e)).card) (λ e, 2) _ rfl, + (λ e, (univ.filter (λ (x : G.dart), dart.edge x = e)).card) (λ e, 2) _ rfl, simp [mul_comm], intros e h, rw mem_edge_finset at h, exact G.dart_edge_fiber_card e h, From bde921ad7e00a990a7bcda19d2988c9db876d16c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 00:58:06 -0800 Subject: [PATCH 29/50] linting --- src/combinatorics/simple_graph/handshake.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index aad710f5b2a32..9a2136341105c 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -51,6 +51,7 @@ structure dart := (edge_mem : edge ∈ G.edge_set) (vert_mem : vert ∈ edge) +/-- There is an equivalence between darts and pairs of a vertex and an incident edge. -/ def dart_equiv_sigma : G.dart ≃ Σ v, G.incidence_set v := { to_fun := λ d, ⟨d.vert, d.edge, d.edge_mem, d.vert_mem⟩, inv_fun := λ s, ⟨s.fst, s.snd, s.snd.property.1, s.snd.property.2⟩, @@ -134,10 +135,10 @@ begin { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart.vert] }, end -lemma dart_card_eq_sum_degrees [hd : decidable_eq V] : fintype.card G.dart = ∑ v, G.degree v := +lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := begin convert_to (univ : finset G.dart).card = _, - rw @card_eq_sum_card_fiberwise _ _ hd dart.vert _ univ (λ d h, mem_univ _), + rw @card_eq_sum_card_fiberwise _ _ (by assumption) dart.vert _ univ (λ d h, mem_univ _), simp [G.dart_vert_fiber_card_eq_degree], end From 810d26f9c5ec3bd16b9fae072701ca0cebd0aa24 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 01:02:45 -0800 Subject: [PATCH 30/50] removed unnecessary lemma --- src/combinatorics/simple_graph/handshake.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 9a2136341105c..54ce273a6be01 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -66,9 +66,6 @@ instance dart.inhabited [inhabited V] [inhabited (G.incidence_set (default _))] variables {G} -lemma dart.edge_mem_incidence_set (d : G.dart) : d.edge ∈ G.incidence_set d.vert := -⟨d.edge_mem, d.vert_mem⟩ - /-- Reverses the orientation of a dart. -/ def dart.rev [decidable_eq V] (d : G.dart) : G.dart := { vert := sym2.mem.other' d.vert_mem, @@ -130,7 +127,7 @@ begin ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, - { rintro rfl, use d.edge, use d.edge_mem_incidence_set, + { rintro rfl, use [d.edge, ⟨d.edge_mem, d.vert_mem⟩], apply dart.ext; simp [dart_from_incidence_set, dart.vert, dart.edge], }, { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart.vert] }, end From 1477cd0c7deae8f389aca7e8bebc6247d9f1b8f0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 03:30:52 -0800 Subject: [PATCH 31/50] unnecessary universe variable --- src/combinatorics/simple_graph/handshake.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 54ce273a6be01..43c8b7d3728d5 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -40,7 +40,7 @@ open finset open_locale big_operators namespace simple_graph -universes u v +universes u variables {V : Type u} (G : simple_graph V) /-- A `dart` is a directed edge, consisting of a vertex and an edge incident to it -/ From c86b037ecf4d5fd36efdc0946626b872ad56e0a0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 03:41:06 -0800 Subject: [PATCH 32/50] Update src/combinatorics/simple_graph/basic.lean Co-authored-by: Eric Wieser --- src/combinatorics/simple_graph/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 8085cf35a2b25..b20a8f6566eab 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -140,7 +140,7 @@ end instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] : fintype G.edge_set := by { dunfold edge_set, exact subtype.fintype _ } -instance mem_edges_decidable [decidable_rel G.adj] (e : sym2 V) : +instance mem_edge_set_decidable [decidable_rel G.adj] (e : sym2 V) : decidable (e ∈ G.edge_set) := by { dunfold edge_set, apply_instance } instance mem_incidence_set_decidable [decidable_eq V] [decidable_rel G.adj] (v : V) (e : sym2 V) : From fafc7b54f50922c4bcde02722cfe03a802afccaa Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 03:41:43 -0800 Subject: [PATCH 33/50] Update src/combinatorics/simple_graph/handshake.lean Co-authored-by: Eric Wieser --- src/combinatorics/simple_graph/handshake.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 54ce273a6be01..0680bd3a58f1e 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -75,13 +75,16 @@ def dart.rev [decidable_eq V] (d : G.dart) : G.dart := @[simp] lemma dart_edge_of_dart_rev [decidable_eq V] (d : G.dart) : d.rev.edge = d.edge := rfl -lemma dart_rev_invol [decidable_eq V] (d : G.dart) : d.rev.rev = d := +@[simp] lemma dart_rev_invol [decidable_eq V] (d : G.dart) : d.rev.rev = d := begin apply dart.ext, apply sym2.other_invol', simp only [dart_edge_of_dart_rev], end +@[simp] lemma dart_rev_involutive [decidable_eq V] : function.involutive (dart.rev : G.dart → G.dart) := +dart_rev_invol + lemma dart_rev_no_fixedpoints [decidable_eq V] (d : G.dart) : d ≠ d.rev := begin intro h, rw dart.ext_iff at h, From 0beb27dd0537e3b265b67ff90b0cbcb8a7c99d1e Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 03:47:19 -0800 Subject: [PATCH 34/50] rename lemmas to use namespace --- src/combinatorics/simple_graph/handshake.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 870bca72d0062..4baf39cfe49cf 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -73,19 +73,19 @@ def dart.rev [decidable_eq V] (d : G.dart) : G.dart := edge_mem := d.edge_mem, vert_mem := sym2.mem_other_mem' d.vert_mem } -@[simp] lemma dart_edge_of_dart_rev [decidable_eq V] (d : G.dart) : d.rev.edge = d.edge := rfl +@[simp] lemma dart.rev_edge_eq [decidable_eq V] (d : G.dart) : d.rev.edge = d.edge := rfl -@[simp] lemma dart_rev_invol [decidable_eq V] (d : G.dart) : d.rev.rev = d := +@[simp] lemma dart.rev_rev_eq [decidable_eq V] (d : G.dart) : d.rev.rev = d := begin apply dart.ext, apply sym2.other_invol', - simp only [dart_edge_of_dart_rev], + simp only [dart.rev_edge_eq], end @[simp] lemma dart_rev_involutive [decidable_eq V] : function.involutive (dart.rev : G.dart → G.dart) := -dart_rev_invol +dart.rev_rev_eq -lemma dart_rev_no_fixedpoints [decidable_eq V] (d : G.dart) : d ≠ d.rev := +lemma dart.neq_rev [decidable_eq V] (d : G.dart) : d ≠ d.rev := begin intro h, rw dart.ext_iff at h, dsimp [dart.vert, dart.rev] at h, @@ -99,7 +99,7 @@ begin have h₁ : d₁.edge = ⟦(d₁.vert, d₁.rev.vert)⟧ := (sym2.mem_other_spec' d₁.vert_mem).symm, have h₂ : d₂.edge = ⟦(d₂.vert, d₂.rev.vert)⟧ := (sym2.mem_other_spec' d₂.vert_mem).symm, split, - { rw [dart.ext_iff, dart.ext_iff, dart_edge_of_dart_rev], + { rw [dart.ext_iff, dart.ext_iff, dart.rev_edge_eq], intro h, simp only [h, and_true, eq_self_iff_true], rw [h₁, h₂, sym2.eq_iff] at h, cases h, @@ -156,7 +156,7 @@ begin refine quotient.ind (λ p h, _) e h, cases p with v w, let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, convert_to _ = finset.card {d, d.rev}, - { rw [card_insert_of_not_mem, card_singleton], simp [dart_rev_no_fixedpoints d], }, + { rw [card_insert_of_not_mem, card_singleton], simp [d.neq_rev], }, congr, apply G.dart_edge_fiber d, end From 95f8b2f725ca12de95757f030e340b711cd64a28 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 03:58:46 -0800 Subject: [PATCH 35/50] eric-wieser golfing --- src/combinatorics/simple_graph/handshake.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 4baf39cfe49cf..c201c949ca81a 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -183,11 +183,7 @@ end degree_sum section TODO_move lemma zmod_eq_zero_iff_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := -begin - change (n : zmod 2) = ((0 : ℕ) : zmod 2) ↔ _, - rw [zmod.eq_iff_modeq_nat, nat.even_iff], - trivial, -end +(char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm lemma zmod_eq_one_iff_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := begin From 9249833e6d9bebd91d5df0339847144b57bdea60 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 04:54:08 -0800 Subject: [PATCH 36/50] (lint) Long line --- src/combinatorics/simple_graph/handshake.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index c201c949ca81a..48db265dc6686 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -82,7 +82,8 @@ begin simp only [dart.rev_edge_eq], end -@[simp] lemma dart_rev_involutive [decidable_eq V] : function.involutive (dart.rev : G.dart → G.dart) := +@[simp] lemma dart_rev_involutive [decidable_eq V] : + function.involutive (dart.rev : G.dart → G.dart) := dart.rev_rev_eq lemma dart.neq_rev [decidable_eq V] (d : G.dart) : d ≠ d.rev := From f9972000a506c582b37e8d3aa4768afcb1c72a3e Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 14:50:07 -0800 Subject: [PATCH 37/50] b-mehta review --- src/combinatorics/simple_graph/handshake.lean | 106 ++++++++++-------- 1 file changed, 58 insertions(+), 48 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 48db265dc6686..9730a18ec9d1f 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -67,19 +67,18 @@ instance dart.inhabited [inhabited V] [inhabited (G.incidence_set (default _))] variables {G} /-- Reverses the orientation of a dart. -/ +@[simps] def dart.rev [decidable_eq V] (d : G.dart) : G.dart := { vert := sym2.mem.other' d.vert_mem, edge := d.edge, edge_mem := d.edge_mem, vert_mem := sym2.mem_other_mem' d.vert_mem } -@[simp] lemma dart.rev_edge_eq [decidable_eq V] (d : G.dart) : d.rev.edge = d.edge := rfl - @[simp] lemma dart.rev_rev_eq [decidable_eq V] (d : G.dart) : d.rev.rev = d := begin apply dart.ext, apply sym2.other_invol', - simp only [dart.rev_edge_eq], + refl, end @[simp] lemma dart_rev_involutive [decidable_eq V] : @@ -88,10 +87,12 @@ dart.rev_rev_eq lemma dart.neq_rev [decidable_eq V] (d : G.dart) : d ≠ d.rev := begin - intro h, rw dart.ext_iff at h, - dsimp [dart.vert, dart.rev] at h, + intro h, + rw dart.ext_iff at h, + dsimp at h, apply G.edge_other_ne d.edge_mem d.vert_mem, - convert h.1.symm, rw sym2.other_eq_other', + convert h.1.symm, + rw sym2.other_eq_other', end lemma dart_edge_eq_iff [decidable_eq V] (d₁ d₂ : G.dart) : @@ -100,24 +101,23 @@ begin have h₁ : d₁.edge = ⟦(d₁.vert, d₁.rev.vert)⟧ := (sym2.mem_other_spec' d₁.vert_mem).symm, have h₂ : d₂.edge = ⟦(d₂.vert, d₂.rev.vert)⟧ := (sym2.mem_other_spec' d₂.vert_mem).symm, split, - { rw [dart.ext_iff, dart.ext_iff, dart.rev_edge_eq], - intro h, simp only [h, and_true, eq_self_iff_true], + { rw [dart.ext_iff, dart.ext_iff, dart.rev_edge], + intro h, + simp only [h, and_true, eq_self_iff_true], rw [h₁, h₂, sym2.eq_iff] at h, - cases h, - { exact or.inl h.1 }, - { exact or.inr h.1 }, }, + apply or.imp and.left and.left h, }, { intro h, cases h; subst d₁, refl, }, end variables (G) /-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ +@[simps] def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := λ ee, ⟨v, ee, ee.property.1, ee.property.2⟩ lemma dart_from_incidence_set_inj (v : V) : function.injective (G.dart_from_incidence_set v) := -by { intros e₁ e₂, dsimp only [dart_from_incidence_set, dart_equiv_sigma], - simp only [true_and, equiv.coe_fn_symm_mk, eq_self_iff_true], exact subtype.ext, } +λ e₁ e₂ h, by { injection h with h₁ h₂, exact subtype.ext h₂ } section degree_sum variables [fintype V] [decidable_eq V] [decidable_rel G.adj] @@ -131,46 +131,44 @@ begin ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, - { rintro rfl, use [d.edge, ⟨d.edge_mem, d.vert_mem⟩], - apply dart.ext; simp [dart_from_incidence_set, dart.vert, dart.edge], }, - { rintro ⟨e, he, rfl⟩, simp [dart_from_incidence_set, dart.vert] }, + { rintro rfl, + exact ⟨_, ⟨d.edge_mem, d.vert_mem⟩, dart.ext _ _ rfl rfl⟩, }, + { rintro ⟨e, he, rfl⟩, + refl, }, end lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := begin - convert_to (univ : finset G.dart).card = _, - rw @card_eq_sum_card_fiberwise _ _ (by assumption) dart.vert _ univ (λ d h, mem_univ _), - simp [G.dart_vert_fiber_card_eq_degree], + simp only [←card_univ, ←G.dart_vert_fiber_card_eq_degree], + exact card_eq_sum_card_fiberwise (by simp), end lemma dart_edge_fiber (d : G.dart) : (univ.filter (λ (d' : G.dart), d'.edge = d.edge)) = {d, d.rev} := -begin - ext d', - simp only [true_and, mem_filter, mem_insert, mem_univ, mem_singleton], - exact dart_edge_eq_iff d' d, -end +finset.ext (λ d', by simpa using dart_edge_eq_iff d' d) lemma dart_edge_fiber_card (e : sym2 V) (h : e ∈ G.edge_set) : (univ.filter (λ (d : G.dart), d.edge = e)).card = 2 := begin - refine quotient.ind (λ p h, _) e h, cases p with v w, + refine quotient.ind (λ p h, _) e h, + cases p with v w, let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, convert_to _ = finset.card {d, d.rev}, - { rw [card_insert_of_not_mem, card_singleton], simp [d.neq_rev], }, - congr, apply G.dart_edge_fiber d, + { rw [card_insert_of_not_mem, card_singleton], + simp [d.neq_rev], }, + congr, + apply G.dart_edge_fiber d, end lemma dart_card_eq_twice_card_edges : fintype.card G.dart = 2 * G.edge_finset.card := begin - convert_to (univ : finset G.dart).card = _, + rw ←card_univ, rw @card_eq_sum_card_fiberwise _ _ _ dart.edge _ G.edge_finset (λ d h, by { rw mem_edge_finset, apply dart.edge_mem }), - rw @sum_congr _ _ G.edge_finset G.edge_finset - (λ e, (univ.filter (λ (x : G.dart), dart.edge x = e)).card) (λ e, 2) _ rfl, - simp [mul_comm], - intros e h, rw mem_edge_finset at h, - exact G.dart_edge_fiber_card e h, + rw [←mul_comm, sum_const_nat], + intros e h, + apply G.dart_edge_fiber_card e, + rwa ←mem_edge_finset, end /-- The degree-sum formula. This is also known as the handshaking lemma, which might @@ -208,12 +206,16 @@ begin rw sum_nat_cast at h, rw ←sum_filter_ne_zero at h, rw @sum_congr _ (zmod 2) _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h, - simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, - rw ←zmod_eq_zero_iff_even, - convert h, - ext v, rw ←zmod_neq_zero_iff_odd, split, intro h, convert h, intro h, convert h, - intros v, simp only [true_and, mem_filter, mem_univ, ne.def], - rw [zmod_eq_zero_iff_even, zmod_eq_one_iff_odd, nat.odd_iff_not_even, imp_self], trivial, + { simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, + rw ←zmod_eq_zero_iff_even, + convert h, + ext v, + rw ←zmod_neq_zero_iff_odd, + congr' }, + { intros v, + simp only [true_and, mem_filter, mem_univ, ne.def], + rw [zmod_eq_zero_iff_even, zmod_eq_one_iff_odd, nat.odd_iff_not_even, imp_self], + trivial } end lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] @@ -223,16 +225,23 @@ begin rcases G.card_odd_degree_vertices_is_even with ⟨k, hg⟩, have hk : 0 < k, { have hh : (filter (λ (v : V), odd (G.degree v)) univ).nonempty, - { use v, simp only [true_and, mem_filter, mem_univ], use h, }, - rw ←card_pos at hh, rw hg at hh, clear hg, linarith, }, + { use v, + simp only [true_and, mem_filter, mem_univ], + use h, }, + rw [←card_pos, hg] at hh, + clear hg, + linarith, }, have hc : (λ (w : V), w ≠ v ∧ odd (G.degree w)) = (λ (w : V), odd (G.degree w) ∧ w ≠ v), - { ext w, rw and_comm, }, + { ext w, + rw and_comm, }, simp only [hc, filter_congr_decidable], - rw [←filter_filter, filter_ne'], - rw card_erase_of_mem, - use k - 1, rw nat.pred_eq_succ_iff, rw hg, clear hc hg, rw nat.mul_sub_left_distrib, omega, - simp only [true_and, mem_filter, mem_univ], - exact h, + rw [←filter_filter, filter_ne', card_erase_of_mem], + { use k - 1, + rw [nat.pred_eq_succ_iff, hg], + clear hc hg, + rw nat.mul_sub_left_distrib, + omega, }, + { simpa only [true_and, mem_filter, mem_univ] }, end lemma exists_ne_odd_degree_if_exists_odd [fintype V] @@ -242,7 +251,8 @@ begin haveI : decidable_eq V := by { classical, apply_instance }, rcases G.card_odd_degree_vertices_ne_is_odd v h with ⟨k, hg⟩, have hg' : (filter (λ (w : V), w ≠ v ∧ odd (G.degree w)) univ).card > 0, - { rw hg, apply nat.succ_pos, }, + { rw hg, + apply nat.succ_pos, }, rcases card_pos.mp hg' with ⟨w, hw⟩, simp only [true_and, mem_filter, mem_univ, ne.def] at hw, exact ⟨w, hw⟩, From a9f779a7998c0b9ce95e5330bb96c6b9a2450713 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 15:25:23 -0800 Subject: [PATCH 38/50] Changed structure for dart to be an ordered pair of adjacent vertices This simplifies a number of things, and it's more natural anyway, given the structure we use for simple graphs. --- src/combinatorics/simple_graph/handshake.lean | 109 +++++++++--------- 1 file changed, 52 insertions(+), 57 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 9730a18ec9d1f..a47e258c0a083 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -17,7 +17,8 @@ a corollary, which is that the number of odd-degree vertices is even. ## Main definitions -- A `dart` is a directed edge, consisting of a vertex and an edge incident to it. +- A `dart` is a directed edge, consisting of an ordered pair of adjacent vertices, + thought of as being a directed edge. - `simple_graph.sum_degrees_eq_twice_card_edges` is the degree-sum formula. - `simple_graph.card_odd_degree_vertices_is_even` is the handshaking lemma. - `simple_graph.card_odd_degree_vertices_ne_is_odd` is that the number of odd-degree @@ -43,106 +44,100 @@ namespace simple_graph universes u variables {V : Type u} (G : simple_graph V) -/-- A `dart` is a directed edge, consisting of a vertex and an edge incident to it -/ +/-- A dart is a directed edge, consisting of an ordered pair of adjacent vertices. -/ @[ext, derive decidable_eq] structure dart := -(vert : V) -(edge : sym2 V) -(edge_mem : edge ∈ G.edge_set) -(vert_mem : vert ∈ edge) +(fst snd : V) +(is_adj : G.adj fst snd) /-- There is an equivalence between darts and pairs of a vertex and an incident edge. -/ -def dart_equiv_sigma : G.dart ≃ Σ v, G.incidence_set v := -{ to_fun := λ d, ⟨d.vert, d.edge, d.edge_mem, d.vert_mem⟩, - inv_fun := λ s, ⟨s.fst, s.snd, s.snd.property.1, s.snd.property.2⟩, - left_inv := λ d, by { ext, simp only, simp only [subtype.coe_mk], }, - right_inv := λ s, by { ext, simp only, simp only [subtype.coe_eta], } } +@[simps] +def dart_equiv_sigma : G.dart ≃ Σ v, G.neighbor_set v := +{ to_fun := λ d, ⟨d.fst, d.snd, d.is_adj⟩, + inv_fun := λ s, ⟨s.fst, s.snd, s.snd.property⟩, + left_inv := λ d, by ext; simp, + right_inv := λ s, by ext; simp } -instance dart.fintype [fintype V] [decidable_eq V] [decidable_rel G.adj] : fintype (dart G) := +instance dart.fintype [fintype V] [decidable_rel G.adj] : fintype G.dart := fintype.of_equiv _ G.dart_equiv_sigma.symm -instance dart.inhabited [inhabited V] [inhabited (G.incidence_set (default _))] : +instance dart.inhabited [inhabited V] [inhabited (G.neighbor_set (default _))] : inhabited G.dart := ⟨G.dart_equiv_sigma.symm ⟨default _, default _⟩⟩ variables {G} +/-- The edge associated to the dart. -/ +def dart.edge (d : G.dart) : sym2 V := ⟦(d.fst, d.snd)⟧ + +@[simp] lemma dart.edge_mem (d : G.dart) : d.edge ∈ G.edge_set := +d.is_adj + /-- Reverses the orientation of a dart. -/ -@[simps] -def dart.rev [decidable_eq V] (d : G.dart) : G.dart := -{ vert := sym2.mem.other' d.vert_mem, - edge := d.edge, - edge_mem := d.edge_mem, - vert_mem := sym2.mem_other_mem' d.vert_mem } +def dart.rev (d : G.dart) : G.dart := +⟨d.snd, d.fst, G.sym d.is_adj⟩ -@[simp] lemma dart.rev_rev_eq [decidable_eq V] (d : G.dart) : d.rev.rev = d := -begin - apply dart.ext, - apply sym2.other_invol', - refl, -end +@[simp] lemma dart.rev_edge (d : G.dart) : d.rev.edge = d.edge := +sym2.eq_swap + +@[simp] lemma dart.rev_rev (d : G.dart) : d.rev.rev = d := +dart.ext _ _ rfl rfl -@[simp] lemma dart_rev_involutive [decidable_eq V] : - function.involutive (dart.rev : G.dart → G.dart) := -dart.rev_rev_eq +@[simp] lemma dart_rev_involutive : function.involutive (dart.rev : G.dart → G.dart) := +dart.rev_rev -lemma dart.neq_rev [decidable_eq V] (d : G.dart) : d ≠ d.rev := +lemma dart.neq_rev (d : G.dart) : d ≠ d.rev := begin - intro h, - rw dart.ext_iff at h, - dsimp at h, - apply G.edge_other_ne d.edge_mem d.vert_mem, - convert h.1.symm, - rw sym2.other_eq_other', + cases d with f s h, + simp [dart.rev], + rintro rfl, + exact false.elim (G.loopless _ h), end -lemma dart_edge_eq_iff [decidable_eq V] (d₁ d₂ : G.dart) : +lemma dart_edge_eq_iff (d₁ d₂ : G.dart) : d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.rev := begin - have h₁ : d₁.edge = ⟦(d₁.vert, d₁.rev.vert)⟧ := (sym2.mem_other_spec' d₁.vert_mem).symm, - have h₂ : d₂.edge = ⟦(d₂.vert, d₂.rev.vert)⟧ := (sym2.mem_other_spec' d₂.vert_mem).symm, - split, - { rw [dart.ext_iff, dart.ext_iff, dart.rev_edge], - intro h, - simp only [h, and_true, eq_self_iff_true], - rw [h₁, h₂, sym2.eq_iff] at h, - apply or.imp and.left and.left h, }, - { intro h, cases h; subst d₁, refl, }, + cases d₁ with s₁ t₁ h₁, + cases d₂ with s₂ t₂ h₂, + simp only [dart.edge, dart.rev_edge, dart.rev], + rw sym2.eq_iff, end variables (G) /-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ -@[simps] -def dart_from_incidence_set (v : V) : G.incidence_set v → G.dart := -λ ee, ⟨v, ee, ee.property.1, ee.property.2⟩ +def dart_from_neighbor_set (v : V) : G.neighbor_set v → G.dart := +λ w, ⟨v, w, w.property⟩ -lemma dart_from_incidence_set_inj (v : V) : function.injective (G.dart_from_incidence_set v) := +lemma dart_from_neighbor_set_inj (v : V) : function.injective (G.dart_from_neighbor_set v) := λ e₁ e₂ h, by { injection h with h₁ h₂, exact subtype.ext h₂ } section degree_sum -variables [fintype V] [decidable_eq V] [decidable_rel G.adj] +variables [fintype V] [decidable_rel G.adj] -lemma dart_vert_fiber_card_eq_degree (v : V) : - (univ.filter (λ d : G.dart, d.vert = v)).card = G.degree v := +lemma dart_vert_fiber_card_eq_degree [decidable_eq V] (v : V) : + (univ.filter (λ d : G.dart, d.fst = v)).card = G.degree v := begin - have hh := card_image_of_injective univ (G.dart_from_incidence_set_inj v), - rw [finset.card_univ, card_incidence_set_eq_degree] at hh, + have hh := card_image_of_injective univ (G.dart_from_neighbor_set_inj v), + rw [finset.card_univ, card_neighbor_set_eq_degree] at hh, convert hh, ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, { rintro rfl, - exact ⟨_, ⟨d.edge_mem, d.vert_mem⟩, dart.ext _ _ rfl rfl⟩, }, + exact ⟨_, d.is_adj, dart.ext _ _ rfl rfl⟩, }, { rintro ⟨e, he, rfl⟩, refl, }, end lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := begin - simp only [←card_univ, ←G.dart_vert_fiber_card_eq_degree], + haveI h : decidable_eq V := by { classical, apply_instance }, + simp only [←card_univ, ←dart_vert_fiber_card_eq_degree], exact card_eq_sum_card_fiberwise (by simp), end +variables [decidable_eq V] + lemma dart_edge_fiber (d : G.dart) : (univ.filter (λ (d' : G.dart), d'.edge = d.edge)) = {d, d.rev} := finset.ext (λ d', by simpa using dart_edge_eq_iff d' d) @@ -152,7 +147,7 @@ lemma dart_edge_fiber_card (e : sym2 V) (h : e ∈ G.edge_set) : begin refine quotient.ind (λ p h, _) e h, cases p with v w, - let d : G.dart := ⟨v, ⟦(v, w)⟧, h, sym2.mk_has_mem _ _⟩, + let d : G.dart := ⟨v, w, h⟩, convert_to _ = finset.card {d, d.rev}, { rw [card_insert_of_not_mem, card_singleton], simp [d.neq_rev], }, From 80e50f3204f8e5a26d66b538d762d7b44d7fc384 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 15:39:36 -0800 Subject: [PATCH 39/50] oops, non-terminal simp --- src/combinatorics/simple_graph/handshake.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index a47e258c0a083..39c9508ed8288 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -85,10 +85,10 @@ dart.ext _ _ rfl rfl @[simp] lemma dart_rev_involutive : function.involutive (dart.rev : G.dart → G.dart) := dart.rev_rev -lemma dart.neq_rev (d : G.dart) : d ≠ d.rev := +lemma dart.rev_ne (d : G.dart) : d.rev ≠ d := begin cases d with f s h, - simp [dart.rev], + simp only [dart.rev, not_and, ne.def], rintro rfl, exact false.elim (G.loopless _ h), end @@ -150,7 +150,8 @@ begin let d : G.dart := ⟨v, w, h⟩, convert_to _ = finset.card {d, d.rev}, { rw [card_insert_of_not_mem, card_singleton], - simp [d.neq_rev], }, + rw [mem_singleton], + exact d.rev_ne.symm, }, congr, apply G.dart_edge_fiber d, end @@ -186,7 +187,7 @@ begin trivial, end -lemma zmod_neq_zero_iff_odd (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := +lemma zmod_ne_zero_iff_odd (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := by split; { contrapose, simp [zmod_eq_zero_iff_even], } end TODO_move @@ -205,7 +206,7 @@ begin rw ←zmod_eq_zero_iff_even, convert h, ext v, - rw ←zmod_neq_zero_iff_odd, + rw ←zmod_ne_zero_iff_odd, congr' }, { intros v, simp only [true_and, mem_filter, mem_univ, ne.def], From f74156eca6be2d649b4914e25c8e87ae376efe05 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 16:49:48 -0800 Subject: [PATCH 40/50] factored out combinatorial part of vert fiber --- src/combinatorics/simple_graph/handshake.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 39c9508ed8288..ab6dbc5257003 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -114,12 +114,9 @@ lemma dart_from_neighbor_set_inj (v : V) : function.injective (G.dart_from_neigh section degree_sum variables [fintype V] [decidable_rel G.adj] -lemma dart_vert_fiber_card_eq_degree [decidable_eq V] (v : V) : - (univ.filter (λ d : G.dart, d.fst = v)).card = G.degree v := +lemma dart_vert_fiber [decidable_eq V] (v : V) : + univ.filter (λ d : G.dart, d.fst = v) = univ.image (G.dart_from_neighbor_set v) := begin - have hh := card_image_of_injective univ (G.dart_from_neighbor_set_inj v), - rw [finset.card_univ, card_neighbor_set_eq_degree] at hh, - convert hh, ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], split, @@ -129,6 +126,14 @@ begin refl, }, end +lemma dart_vert_fiber_card_eq_degree [decidable_eq V] (v : V) : + (univ.filter (λ d : G.dart, d.fst = v)).card = G.degree v := +begin + have hh := card_image_of_injective univ (G.dart_from_neighbor_set_inj v), + rw [finset.card_univ, card_neighbor_set_eq_degree] at hh, + rwa dart_vert_fiber, +end + lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := begin haveI h : decidable_eq V := by { classical, apply_instance }, From 7c2bf0ec90787b0b0c7a7cd3317398173cc43627 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 7 Dec 2020 16:51:02 -0800 Subject: [PATCH 41/50] naming vert -> fst to match struct --- src/combinatorics/simple_graph/handshake.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index ab6dbc5257003..66b499b5dfdbe 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -114,7 +114,7 @@ lemma dart_from_neighbor_set_inj (v : V) : function.injective (G.dart_from_neigh section degree_sum variables [fintype V] [decidable_rel G.adj] -lemma dart_vert_fiber [decidable_eq V] (v : V) : +lemma dart_fst_fiber [decidable_eq V] (v : V) : univ.filter (λ d : G.dart, d.fst = v) = univ.image (G.dart_from_neighbor_set v) := begin ext d, @@ -126,18 +126,18 @@ begin refl, }, end -lemma dart_vert_fiber_card_eq_degree [decidable_eq V] (v : V) : +lemma dart_fst_fiber_card_eq_degree [decidable_eq V] (v : V) : (univ.filter (λ d : G.dart, d.fst = v)).card = G.degree v := begin have hh := card_image_of_injective univ (G.dart_from_neighbor_set_inj v), rw [finset.card_univ, card_neighbor_set_eq_degree] at hh, - rwa dart_vert_fiber, + rwa dart_fst_fiber, end lemma dart_card_eq_sum_degrees : fintype.card G.dart = ∑ v, G.degree v := begin haveI h : decidable_eq V := by { classical, apply_instance }, - simp only [←card_univ, ←dart_vert_fiber_card_eq_degree], + simp only [←card_univ, ←dart_fst_fiber_card_eq_degree], exact card_eq_sum_card_fiberwise (by simp), end From 19b3f6c24ff8b684bf979bad078ae770680a2e73 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:17:16 -0800 Subject: [PATCH 42/50] bryangingechen naming suggestions --- src/combinatorics/simple_graph/handshake.lean | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/handshake.lean index 66b499b5dfdbe..8e35549807817 100644 --- a/src/combinatorics/simple_graph/handshake.lean +++ b/src/combinatorics/simple_graph/handshake.lean @@ -20,10 +20,10 @@ a corollary, which is that the number of odd-degree vertices is even. - A `dart` is a directed edge, consisting of an ordered pair of adjacent vertices, thought of as being a directed edge. - `simple_graph.sum_degrees_eq_twice_card_edges` is the degree-sum formula. -- `simple_graph.card_odd_degree_vertices_is_even` is the handshaking lemma. -- `simple_graph.card_odd_degree_vertices_ne_is_odd` is that the number of odd-degree +- `simple_graph.even_card_odd_degree_vertices` is the handshaking lemma. +- `simple_graph.odd_card_odd_degree_vertices_ne` is that the number of odd-degree vertices different from a given odd-degree vertex is odd. -- `simple_graph.exists_ne_odd_degree_if_exists_odd` is that the existence of an +- `simple_graph.exists_ne_odd_degree_of_exists_odd_degree` is that the existence of an odd-degree vertex implies the existence of another one. ## Implementation notes @@ -105,17 +105,17 @@ end variables (G) /-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ -def dart_from_neighbor_set (v : V) : G.neighbor_set v → G.dart := -λ w, ⟨v, w, w.property⟩ +def dart_of_neighbor_set (v : V) (w : G.neighbor_set v) : G.dart := +⟨v, w, w.property⟩ -lemma dart_from_neighbor_set_inj (v : V) : function.injective (G.dart_from_neighbor_set v) := +lemma dart_of_neighbor_set_injective (v : V) : function.injective (G.dart_of_neighbor_set v) := λ e₁ e₂ h, by { injection h with h₁ h₂, exact subtype.ext h₂ } section degree_sum variables [fintype V] [decidable_rel G.adj] lemma dart_fst_fiber [decidable_eq V] (v : V) : - univ.filter (λ d : G.dart, d.fst = v) = univ.image (G.dart_from_neighbor_set v) := + univ.filter (λ d : G.dart, d.fst = v) = univ.image (G.dart_of_neighbor_set v) := begin ext d, simp only [mem_image, true_and, mem_filter, set_coe.exists, mem_univ, exists_prop_of_true], @@ -129,7 +129,7 @@ end lemma dart_fst_fiber_card_eq_degree [decidable_eq V] (v : V) : (univ.filter (λ d : G.dart, d.fst = v)).card = G.degree v := begin - have hh := card_image_of_injective univ (G.dart_from_neighbor_set_inj v), + have hh := card_image_of_injective univ (G.dart_of_neighbor_set_injective v), rw [finset.card_univ, card_neighbor_set_eq_degree] at hh, rwa dart_fst_fiber, end @@ -173,7 +173,7 @@ begin end /-- The degree-sum formula. This is also known as the handshaking lemma, which might -more specifically refer to `simple_graph.card_odd_degree_vertices_is_even`. -/ +more specifically refer to `simple_graph.even_card_odd_degree_vertices`. -/ theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * G.edge_finset.card := G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges @@ -182,23 +182,23 @@ end degree_sum section TODO_move -lemma zmod_eq_zero_iff_even (n : ℕ) : (n : zmod 2) = 0 ↔ even n := +lemma zmod_eq_zero_iff_even {n : ℕ} : (n : zmod 2) = 0 ↔ even n := (char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm -lemma zmod_eq_one_iff_odd (n : ℕ) : (n : zmod 2) = 1 ↔ odd n := +lemma zmod_eq_one_iff_odd {n : ℕ} : (n : zmod 2) = 1 ↔ odd n := begin change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, rw [zmod.eq_iff_modeq_nat, nat.odd_iff], trivial, end -lemma zmod_ne_zero_iff_odd (n : ℕ) : (n : zmod 2) ≠ 0 ↔ odd n := +lemma zmod_ne_zero_iff_odd {n : ℕ} : (n : zmod 2) ≠ 0 ↔ odd n := by split; { contrapose, simp [zmod_eq_zero_iff_even], } end TODO_move /-- The handshaking lemma. See also `simple_graph.sum_degrees_eq_twice_card_edges`. -/ -theorem card_odd_degree_vertices_is_even [fintype V] : +theorem even_card_odd_degree_vertices [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := begin classical, @@ -219,11 +219,11 @@ begin trivial } end -lemma card_odd_degree_vertices_ne_is_odd [fintype V] [decidable_eq V] +lemma odd_card_odd_degree_vertices_ne [fintype V] [decidable_eq V] (v : V) (h : odd (G.degree v)) : odd (univ.filter (λ w, w ≠ v ∧ odd (G.degree w))).card := begin - rcases G.card_odd_degree_vertices_is_even with ⟨k, hg⟩, + rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩, have hk : 0 < k, { have hh : (filter (λ (v : V), odd (G.degree v)) univ).nonempty, { use v, @@ -245,12 +245,12 @@ begin { simpa only [true_and, mem_filter, mem_univ] }, end -lemma exists_ne_odd_degree_if_exists_odd [fintype V] +lemma exists_ne_odd_degree_of_exists_odd_degree [fintype V] (v : V) (h : odd (G.degree v)) : ∃ (w : V), w ≠ v ∧ odd (G.degree w) := begin haveI : decidable_eq V := by { classical, apply_instance }, - rcases G.card_odd_degree_vertices_ne_is_odd v h with ⟨k, hg⟩, + rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩, have hg' : (filter (λ (w : V), w ≠ v ∧ odd (G.degree w)) univ).card > 0, { rw hg, apply nat.succ_pos, }, From fbe5d495871ae0f6c1dc6f59c493a7f0ee5c9ed2 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:20:02 -0800 Subject: [PATCH 43/50] renamed handshake.lean to degree_sum.lean --- .../simple_graph/{handshake.lean => degree_sum.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/combinatorics/simple_graph/{handshake.lean => degree_sum.lean} (100%) diff --git a/src/combinatorics/simple_graph/handshake.lean b/src/combinatorics/simple_graph/degree_sum.lean similarity index 100% rename from src/combinatorics/simple_graph/handshake.lean rename to src/combinatorics/simple_graph/degree_sum.lean From fa8f39d9369ae74498d48588eb0b14a72f641ef9 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:25:03 -0800 Subject: [PATCH 44/50] moved parity lemmas --- .../simple_graph/degree_sum.lean | 24 +++---------------- src/data/nat/parity.lean | 18 ++++++++++++++ 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index 8e35549807817..ec0271bbff4ab 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -179,24 +179,6 @@ G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges end degree_sum - -section TODO_move - -lemma zmod_eq_zero_iff_even {n : ℕ} : (n : zmod 2) = 0 ↔ even n := -(char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm - -lemma zmod_eq_one_iff_odd {n : ℕ} : (n : zmod 2) = 1 ↔ odd n := -begin - change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, - rw [zmod.eq_iff_modeq_nat, nat.odd_iff], - trivial, -end - -lemma zmod_ne_zero_iff_odd {n : ℕ} : (n : zmod 2) ≠ 0 ↔ odd n := -by split; { contrapose, simp [zmod_eq_zero_iff_even], } - -end TODO_move - /-- The handshaking lemma. See also `simple_graph.sum_degrees_eq_twice_card_edges`. -/ theorem even_card_odd_degree_vertices [fintype V] : even (univ.filter (λ v, odd (G.degree v))).card := @@ -208,14 +190,14 @@ begin rw ←sum_filter_ne_zero at h, rw @sum_congr _ (zmod 2) _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h, { simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, - rw ←zmod_eq_zero_iff_even, + rw ←zmod.eq_zero_iff_even, convert h, ext v, - rw ←zmod_ne_zero_iff_odd, + rw ←zmod.ne_zero_iff_odd, congr' }, { intros v, simp only [true_and, mem_filter, mem_univ, ne.def], - rw [zmod_eq_zero_iff_even, zmod_eq_one_iff_odd, nat.odd_iff_not_even, imp_self], + rw [zmod.eq_zero_iff_even, zmod.eq_one_iff_odd, nat.odd_iff_not_even, imp_self], trivial } end diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index dcbd11ecb29cb..8d4067404f8d3 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -6,6 +6,7 @@ Authors: Jeremy Avigad The `even` and `odd` predicates on the natural numbers. -/ import data.nat.modeq +import data.zmod.basic namespace nat @@ -130,3 +131,20 @@ example : ¬ even 25394535 := by simp end nat + +namespace zmod + +lemma eq_zero_iff_even {n : ℕ} : (n : zmod 2) = 0 ↔ even n := +(char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm + +lemma eq_one_iff_odd {n : ℕ} : (n : zmod 2) = 1 ↔ odd n := +begin + change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, + rw [zmod.eq_iff_modeq_nat, nat.odd_iff], + trivial, +end + +lemma ne_zero_iff_odd {n : ℕ} : (n : zmod 2) ≠ 0 ↔ odd n := +by split; { contrapose, simp [eq_zero_iff_even], } + +end zmod From 575be73310dbf099c5667a48712d0144551c3087 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:45:11 -0800 Subject: [PATCH 45/50] It turns out there are two definitions of prime, so it broke --- .../simple_graph/degree_sum.lean | 4 +-- src/data/nat/parity.lean | 17 ---------- src/data/zmod/parity.lean | 32 +++++++++++++++++++ 3 files changed, 34 insertions(+), 19 deletions(-) create mode 100644 src/data/zmod/parity.lean diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index ec0271bbff4ab..9143ad906366a 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -1,12 +1,12 @@ /- Copyright (c) 2020 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Kyle Miller. +Author: Kyle Miller -/ import combinatorics.simple_graph.basic import algebra.big_operators.basic import data.nat.parity -import data.zmod.basic +import data.zmod.parity import tactic.omega /-! # Degree-sum formula and handshaking lemma diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index 8d4067404f8d3..619634677e242 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -131,20 +131,3 @@ example : ¬ even 25394535 := by simp end nat - -namespace zmod - -lemma eq_zero_iff_even {n : ℕ} : (n : zmod 2) = 0 ↔ even n := -(char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm - -lemma eq_one_iff_odd {n : ℕ} : (n : zmod 2) = 1 ↔ odd n := -begin - change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, - rw [zmod.eq_iff_modeq_nat, nat.odd_iff], - trivial, -end - -lemma ne_zero_iff_odd {n : ℕ} : (n : zmod 2) ≠ 0 ↔ odd n := -by split; { contrapose, simp [eq_zero_iff_even], } - -end zmod diff --git a/src/data/zmod/parity.lean b/src/data/zmod/parity.lean new file mode 100644 index 0000000000000..cbb144f0302d0 --- /dev/null +++ b/src/data/zmod/parity.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2020 Kyle Miller. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Kyle Miller +-/ +import data.nat.parity +/-! +# Relating parity to natural numbers mod 2 + +This module provides lemmas relating `zmod 2` to `even` and `odd`. + +## Tags + +parity, zmod, even, odd +-/ + +namespace zmod + +lemma eq_zero_iff_even {n : ℕ} : (n : zmod 2) = 0 ↔ even n := +(char_p.cast_eq_zero_iff (zmod 2) 2 n).trans even_iff_two_dvd.symm + +lemma eq_one_iff_odd {n : ℕ} : (n : zmod 2) = 1 ↔ odd n := +begin + change (n : zmod 2) = ((1 : ℕ) : zmod 2) ↔ _, + rw [zmod.eq_iff_modeq_nat, nat.odd_iff], + trivial, +end + +lemma ne_zero_iff_odd {n : ℕ} : (n : zmod 2) ≠ 0 ↔ odd n := +by split; { contrapose, simp [eq_zero_iff_even], } + +end zmod From 504bf77ede6e56425af3bde5ddfd88f4cf80a3b0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:46:44 -0800 Subject: [PATCH 46/50] forgot to remove import from data.nat.parity --- src/data/nat/parity.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/data/nat/parity.lean b/src/data/nat/parity.lean index 619634677e242..dcbd11ecb29cb 100644 --- a/src/data/nat/parity.lean +++ b/src/data/nat/parity.lean @@ -6,7 +6,6 @@ Authors: Jeremy Avigad The `even` and `odd` predicates on the natural numbers. -/ import data.nat.modeq -import data.zmod.basic namespace nat From ca3e4e54d90bbf65a140282264ae4b03591de410 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 01:47:51 -0800 Subject: [PATCH 47/50] and forgot to add that import to data.zmod.parity --- src/data/zmod/parity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/data/zmod/parity.lean b/src/data/zmod/parity.lean index cbb144f0302d0..eb6fabc4074b7 100644 --- a/src/data/zmod/parity.lean +++ b/src/data/zmod/parity.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Kyle Miller -/ import data.nat.parity +import data.zmod.basic /-! # Relating parity to natural numbers mod 2 From 80fd5f90c7beb9ef357b2026fe8fc97be7aa40be Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 17:36:24 -0800 Subject: [PATCH 48/50] eric-wieser suggestion, also changed inhabited instance to not use equiv I'm doing this from my laptop, which doesn't have lean installed, so this might take another commit if I made a mistake. --- src/combinatorics/simple_graph/degree_sum.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index 9143ad906366a..c43a9d025b906 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -61,9 +61,6 @@ def dart_equiv_sigma : G.dart ≃ Σ v, G.neighbor_set v := instance dart.fintype [fintype V] [decidable_rel G.adj] : fintype G.dart := fintype.of_equiv _ G.dart_equiv_sigma.symm -instance dart.inhabited [inhabited V] [inhabited (G.neighbor_set (default _))] : - inhabited G.dart := ⟨G.dart_equiv_sigma.symm ⟨default _, default _⟩⟩ - variables {G} /-- The edge associated to the dart. -/ @@ -82,7 +79,7 @@ sym2.eq_swap @[simp] lemma dart.rev_rev (d : G.dart) : d.rev.rev = d := dart.ext _ _ rfl rfl -@[simp] lemma dart_rev_involutive : function.involutive (dart.rev : G.dart → G.dart) := +@[simp] lemma dart.rev_involutive : function.involutive (dart.rev : G.dart → G.dart) := dart.rev_rev lemma dart.rev_ne (d : G.dart) : d.rev ≠ d := @@ -111,6 +108,9 @@ def dart_of_neighbor_set (v : V) (w : G.neighbor_set v) : G.dart := lemma dart_of_neighbor_set_injective (v : V) : function.injective (G.dart_of_neighbor_set v) := λ e₁ e₂ h, by { injection h with h₁ h₂, exact subtype.ext h₂ } +instance dart.inhabited [inhabited V] [inhabited (G.neighbor_set (default _))] : + inhabited G.dart := G.dart_of_neighbor_set (default _) (default _) + section degree_sum variables [fintype V] [decidable_rel G.adj] From fa68921f938544754bacd3826e8d9ebbedb0042b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 8 Dec 2020 17:41:30 -0800 Subject: [PATCH 49/50] added missing brackets (doing this from a plain text editor) --- src/combinatorics/simple_graph/degree_sum.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index c43a9d025b906..3b3d440101c7b 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -109,7 +109,7 @@ lemma dart_of_neighbor_set_injective (v : V) : function.injective (G.dart_of_nei λ e₁ e₂ h, by { injection h with h₁ h₂, exact subtype.ext h₂ } instance dart.inhabited [inhabited V] [inhabited (G.neighbor_set (default _))] : - inhabited G.dart := G.dart_of_neighbor_set (default _) (default _) + inhabited G.dart := ⟨G.dart_of_neighbor_set (default _) (default _)⟩ section degree_sum variables [fintype V] [decidable_rel G.adj] From e661cd41a3d3ef2ff5214aa34b208e4fd21ac9ac Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 10 Dec 2020 17:24:05 -0800 Subject: [PATCH 50/50] documentation, some cleanup, some eric-wieser suggestions --- .../simple_graph/degree_sum.lean | 59 ++++++++----------- 1 file changed, 26 insertions(+), 33 deletions(-) diff --git a/src/combinatorics/simple_graph/degree_sum.lean b/src/combinatorics/simple_graph/degree_sum.lean index 3b3d440101c7b..d819c1a1625e8 100644 --- a/src/combinatorics/simple_graph/degree_sum.lean +++ b/src/combinatorics/simple_graph/degree_sum.lean @@ -11,9 +11,9 @@ import tactic.omega /-! # Degree-sum formula and handshaking lemma -The degree-sum formula is that the sum of the degrees of a finite -graph is equal to twice the number of edges. The handshaking lemma is -a corollary, which is that the number of odd-degree vertices is even. +The degree-sum formula is that the sum of the degrees of the vertices in +a finite graph is equal to twice the number of edges. The handshaking lemma, +a corollary, is that the number of odd-degree vertices is even. ## Main definitions @@ -28,9 +28,9 @@ a corollary, which is that the number of odd-degree vertices is even. ## Implementation notes -We give a combinatorial proof by using the fact that the map from -darts to vertices has fibers whose cardinalities are the degrees and -that the map from darts to edges is 2-to-1. +We give a combinatorial proof by using the facts that (1) the map from +darts to vertices is such that each fiber has cardinality the degree +of the corresponding vertex and that (2) the map from darts to edges is 2-to-1. ## Tags @@ -50,16 +50,12 @@ structure dart := (fst snd : V) (is_adj : G.adj fst snd) -/-- There is an equivalence between darts and pairs of a vertex and an incident edge. -/ -@[simps] -def dart_equiv_sigma : G.dart ≃ Σ v, G.neighbor_set v := -{ to_fun := λ d, ⟨d.fst, d.snd, d.is_adj⟩, - inv_fun := λ s, ⟨s.fst, s.snd, s.snd.property⟩, - left_inv := λ d, by ext; simp, - right_inv := λ s, by ext; simp } - instance dart.fintype [fintype V] [decidable_rel G.adj] : fintype G.dart := -fintype.of_equiv _ G.dart_equiv_sigma.symm +fintype.of_equiv (Σ v, G.neighbor_set v) +{ to_fun := λ s, ⟨s.fst, s.snd, s.snd.property⟩, + inv_fun := λ d, ⟨d.fst, d.snd, d.is_adj⟩, + left_inv := λ s, by ext; simp, + right_inv := λ d, by ext; simp } variables {G} @@ -69,7 +65,7 @@ def dart.edge (d : G.dart) : sym2 V := ⟦(d.fst, d.snd)⟧ @[simp] lemma dart.edge_mem (d : G.dart) : d.edge ∈ G.edge_set := d.is_adj -/-- Reverses the orientation of a dart. -/ +/-- The dart with reversed orientation from a given dart. -/ def dart.rev (d : G.dart) : G.dart := ⟨d.snd, d.fst, G.sym d.is_adj⟩ @@ -101,7 +97,8 @@ end variables (G) -/-- For a given vertex `v`, the injective map from the incidence set at `v` to the darts there. --/ +/-- For a given vertex `v`, this is the bijective map from the neighbor set at `v` +to the darts `d` with `d.fst = v`. --/ def dart_of_neighbor_set (v : V) (w : G.neighbor_set v) : G.dart := ⟨v, w, w.property⟩ @@ -141,24 +138,24 @@ begin exact card_eq_sum_card_fiberwise (by simp), end -variables [decidable_eq V] +variables {G} [decidable_eq V] -lemma dart_edge_fiber (d : G.dart) : +lemma dart.edge_fiber (d : G.dart) : (univ.filter (λ (d' : G.dart), d'.edge = d.edge)) = {d, d.rev} := finset.ext (λ d', by simpa using dart_edge_eq_iff d' d) +variables (G) + lemma dart_edge_fiber_card (e : sym2 V) (h : e ∈ G.edge_set) : (univ.filter (λ (d : G.dart), d.edge = e)).card = 2 := begin refine quotient.ind (λ p h, _) e h, cases p with v w, let d : G.dart := ⟨v, w, h⟩, - convert_to _ = finset.card {d, d.rev}, - { rw [card_insert_of_not_mem, card_singleton], - rw [mem_singleton], - exact d.rev_ne.symm, }, - congr, - apply G.dart_edge_fiber d, + convert congr_arg card d.edge_fiber, + rw [card_insert_of_not_mem, card_singleton], + rw [mem_singleton], + exact d.rev_ne.symm, end lemma dart_card_eq_twice_card_edges : fintype.card G.dart = 2 * G.edge_finset.card := @@ -186,8 +183,7 @@ begin classical, have h := congr_arg ((λ n, ↑n) : ℕ → zmod 2) G.sum_degrees_eq_twice_card_edges, simp only [zmod.cast_self, zero_mul, nat.cast_mul] at h, - rw sum_nat_cast at h, - rw ←sum_filter_ne_zero at h, + rw [sum_nat_cast, ←sum_filter_ne_zero] at h, rw @sum_congr _ (zmod 2) _ _ (λ v, (G.degree v : zmod 2)) (λ v, (1 : zmod 2)) _ rfl at h, { simp only [filter_congr_decidable, mul_one, nsmul_eq_mul, sum_const, ne.def] at h, rw ←zmod.eq_zero_iff_even, @@ -211,18 +207,15 @@ begin { use v, simp only [true_and, mem_filter, mem_univ], use h, }, - rw [←card_pos, hg] at hh, - clear hg, - linarith, }, + rwa [←card_pos, hg, zero_lt_mul_left] at hh, + exact zero_lt_two, }, have hc : (λ (w : V), w ≠ v ∧ odd (G.degree w)) = (λ (w : V), odd (G.degree w) ∧ w ≠ v), { ext w, rw and_comm, }, simp only [hc, filter_congr_decidable], rw [←filter_filter, filter_ne', card_erase_of_mem], { use k - 1, - rw [nat.pred_eq_succ_iff, hg], - clear hc hg, - rw nat.mul_sub_left_distrib, + rw [nat.pred_eq_succ_iff, hg, nat.mul_sub_left_distrib], omega, }, { simpa only [true_and, mem_filter, mem_univ] }, end