Created
May 30, 2019 10:59
-
-
Save avigad/6c1b7a2b771ac561425f50ffd69a4815 to your computer and use it in GitHub Desktop.
a construction of the Mycielskian (https://en.wikipedia.org/wiki/Mycielskian)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import data.fintype tactic.ring | |
structure graph := | |
(vertex : Type*) | |
(edge : vertex → vertex → bool) | |
namespace graph | |
class undirected (G : graph) := | |
(symm : ∀ x y : G.vertex, G.edge x y = G.edge y x) | |
protected def symm {G : graph} [undirected G] : ∀ x y, G.edge x y = G.edge y x := | |
undirected.symm | |
structure coloring (G : graph) (α : Type*) := | |
(func : G.vertex → α) | |
(nonadj : ∀ {x y : G.vertex}, G.edge x y = tt → func x ≠ func y) | |
instance {G : graph} {α : Type*} : has_coe_to_fun (coloring G α) := | |
⟨λ c, G.vertex → α, λ c, c.func⟩ | |
def colorable (G : graph) (k : nat) := | |
∃ (α : Type*) [h : fintype α] [decidable_eq α] (c : coloring G α), @fintype.card α h = k | |
def is_triangle {G : graph} (x y z : G.vertex) : bool := | |
G.edge x y && G.edge y z && G.edge z x | |
end graph | |
section | |
inductive mvertex (α : Type*) | |
| orig : α → mvertex | |
| copy : α → mvertex | |
| hub {} : mvertex | |
open graph mvertex fintype | |
def mvertex_equiv (α : Type*) : mvertex α ≃ (α ⊕ α ⊕ unit) := | |
{ to_fun := λ v, match v with | |
| (orig x) := sum.inl x | |
| (copy x) := sum.inr (sum.inl x) | |
| hub := sum.inr (sum.inr ()) | |
end, | |
inv_fun := λ v, match v with | |
| (sum.inl x) := orig x | |
| (sum.inr (sum.inl x)) := copy x | |
| (sum.inr (sum.inr _)) := hub | |
end, | |
left_inv := by { intro v, cases v; refl }, | |
right_inv := by { intro v, repeat { cases v, refl } } } | |
instance (α : Type*) [h : fintype α] : fintype (mvertex α) := | |
fintype.of_equiv _ (mvertex_equiv α).symm | |
theorem card_mvertex (α : Type*) [fintype α] : card (mvertex α) = 2 * card α + 1 := | |
(card_congr (mvertex_equiv α)).trans (by simp; ring) | |
def medge (G : graph) : mvertex G.vertex → mvertex G.vertex → bool | |
| hub hub := ff | |
| hub (orig y) := ff | |
| (orig x) hub := ff | |
| hub (copy y) := tt | |
| (copy x) hub := tt | |
| (orig x) (orig y) := G.edge x y | |
| (orig x) (copy y) := G.edge x y | |
| (copy x) (orig y) := G.edge x y | |
| (copy x) (copy y) := ff | |
def mycielskian (G : graph) : graph := | |
{ vertex := mvertex G.vertex, | |
edge := medge G } | |
theorem edge_mycielskian (G : graph) : (mycielskian G).edge = medge G := | |
rfl | |
instance fintype_vertex_mycielskian (G : graph) [fintype G.vertex] : | |
fintype (mycielskian G).vertex := | |
by { unfold mycielskian, apply_instance } | |
@[instance] | |
def undirected_mycielskian (G : graph) [h : undirected G] : undirected (mycielskian G) := | |
begin | |
constructor, | |
intro x; cases x; intro y; cases y; dsimp [mycielskian, medge]; refl <|> apply graph.symm | |
end | |
theorem card_mycielskian (G : graph) [fintype G.vertex] : | |
card (mycielskian G).vertex = 2 * card G.vertex + 1 := | |
card_mvertex _ | |
theorem exists_triangle_of_exists_triangle_mycielskian {G : graph} | |
(h : ∃ x y z : (mycielskian G).vertex, is_triangle x y z) : | |
∃ x y z : G.vertex, is_triangle x y z := | |
begin | |
rcases h with ⟨x | x | _, y | y | _, z | z | _, h⟩; | |
simp [is_triangle, edge_mycielskian, medge] at h; try { contradiction }; | |
use [x, y, z]; simp [is_triangle, h] | |
end | |
private def aux {G : graph} {α : Type*} [decidable_eq α] (f : (mycielskian G).vertex → α) : | |
G.vertex → α := | |
λ x, if f (orig x) = f hub then f (copy x) else f (orig x) | |
private theorem aux' {G : graph} {α : Type*} [decidable_eq α] (c : coloring (mycielskian G) α) : | |
∀ x : G.vertex, aux c x ≠ c hub := | |
begin | |
intro x, by_cases h : c (orig x) = c hub; simp [aux, h], | |
apply c.nonadj, refl | |
end | |
theorem coloring_of_coloring_mycielskian {G : graph} {α : Type*} [decidable_eq α] | |
(c : coloring (mycielskian G) α) : | |
coloring G {a // a ≠ c hub} := | |
{ func := λ a, ⟨aux c a, aux' c a⟩, | |
nonadj := (λ x y h h', | |
have h₁ : aux c x = aux c y, | |
from subtype.mk_eq_mk.1 h', | |
begin | |
by_cases h₂ : c (orig x) = c hub; by_cases h₃ : c (orig y) = c hub, | |
{ apply c.nonadj _ (h₂.trans h₃.symm), exact h }, | |
repeat { simp [aux, h₂, h₃] at h₁, apply c.nonadj _ h₁, exact h } | |
end) } | |
theorem {u v} colorable_of_colorable_mycielskian {G : graph.{u}} {k : ℕ} : | |
colorable.{u v} (mycielskian G) (k + 1) → colorable.{u v} G k := | |
begin | |
rintros ⟨α, finα, deceqα, c, cardα⟩, | |
haveI := finα, haveI := deceqα, | |
refine ⟨{a // a ≠ c hub}, _, _, coloring_of_coloring_mycielskian c, _⟩, | |
repeat { apply_instance }, | |
calc | |
card {a // a ≠ c hub} | |
= finset.card (@finset.univ α _ \ {c hub}) : | |
by { rw subtype_card, congr, ext, simp, refl } | |
... = k + 1 - 1 : | |
by { rw [finset.card_sdiff (finset.subset_univ _), finset.card_univ], | |
congr, convert cardα } | |
... = k : rfl | |
end | |
def iterated_mycielskian (G : graph) : ℕ → graph | |
| 0 := G | |
| (n+1) := mycielskian (iterated_mycielskian n) | |
theorem {u v} colorable_of_colorable_iterated_mycielskian {G : graph.{u}} {k n : ℕ} : | |
colorable.{u v} (iterated_mycielskian G n) (k + n) → colorable.{u v} G k := | |
by { induction n with n ih, exact id, exact ih ∘ colorable_of_colorable_mycielskian } | |
theorem exists_triangle_of_exists_triangle_iterated_mycielskian {G : graph} {n : ℕ} : | |
(∃ x y z : (iterated_mycielskian G n).vertex, is_triangle x y z) → | |
∃ x y z : G.vertex, is_triangle x y z := | |
by { induction n with n ih, exact id, exact ih ∘ exists_triangle_of_exists_triangle_mycielskian } | |
instance fintype_vertex_iterated_mycielskian (G : graph) [fintype G.vertex] (n : ℕ): | |
fintype (iterated_mycielskian G n).vertex := | |
by { induction n with n ih, assumption, exact @fintype_vertex_mycielskian _ ih } | |
theorem card_iterated_mycielskian (G : graph) [fintype G.vertex] (n : ℕ) : | |
card (iterated_mycielskian G n).vertex = 2^n * (card G.vertex + 1) - 1 := | |
begin | |
induction n with n ih; simp [iterated_mycielskian], | |
rw [card_mycielskian, ih, nat.pow_succ, nat.left_distrib, nat.left_distrib, | |
nat.mul_sub_left_distrib], ring, | |
rw [nat.sub_add_eq_add_sub], | |
{ apply nat.succ_sub_succ }, | |
change 2 * 1 ≤ _, apply mul_le_mul; try {simp}, | |
change 2^0 ≤ _, apply nat.pow_le_pow_of_le_right; norm_num | |
end | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment