diff options
| -rw-r--r-- | .envrc | 1 | ||||
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Brooks.lean | 187 | ||||
| -rw-r--r-- | flake.lock | 113 | ||||
| -rw-r--r-- | flake.nix | 50 | ||||
| -rw-r--r-- | lake-manifest.json | 95 | ||||
| -rw-r--r-- | lakefile.toml | 10 | ||||
| -rw-r--r-- | lean-toolchain | 1 |
8 files changed, 459 insertions, 0 deletions
diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..27d3834 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.direnv/ +.lake/ diff --git a/Brooks.lean b/Brooks.lean new file mode 100644 index 0000000..24c6daa --- /dev/null +++ b/Brooks.lean @@ -0,0 +1,187 @@ +import Mathlib.Combinatorics.SimpleGraph.Basic +import Mathlib.Combinatorics.SimpleGraph.Finite +import Mathlib.Combinatorics.SimpleGraph.Coloring +import Mathlib.Combinatorics.SimpleGraph.Subgraph +import Mathlib.Combinatorics.SimpleGraph.Path +import Mathlib.Combinatorics.SimpleGraph.Walk +import Mathlib.Combinatorics.SimpleGraph.Maps +import Mathlib.Order.Disjoint +import Mathlib.Data.List.Basic +import Mathlib.Data.List.Lemmas +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.Fintype.Sets +import Mathlib.Data.Set.Basic +import Mathlib.Tactic.Linarith + +open SimpleGraph List Walk Set.Notation +open Classical + +variable + {α : Type} + {V : Type} [Fintype V] + (G : SimpleGraph V) [DecidableRel G.Adj] + +namespace List + abbrev toSet (l : List α) := { x | x ∈ l } + + lemma toSet_nil : ([] : List α).toSet = ∅ := by + simp_all only [toSet, not_mem_nil, Set.setOf_false] + +noncomputable def extend_coloring + (S : Set V) (S_coloring : Coloring (G.induce S) α) + (v : V) (c : α) + (h : c ∉ S_coloring '' (S ↓∩ G.neighborSet v)) + : Coloring (G.induce (S ∪ {v})) α + := by + simp at h + apply Coloring.mk + case color => + intro ⟨x, mem⟩ + by_cases hx : x ∈ S + · exact S_coloring ⟨x, hx⟩ + · exact c + case valid => + rintro ⟨x₁, mem_x₁⟩ ⟨x₂, mem_x₂⟩ + intro adj + by_cases hx₁ : x₁ ∈ S <;> by_cases hx₂ : x₂ ∈ S + -- 4 cases according to whether x₁ and/or x₂ are in S or not + · simp [hx₁, hx₂] + exact S_coloring.valid adj + · simp [hx₁, hx₂] + replace hx₂ : x₂ = v := mem_x₂.resolve_left hx₂ + simp [hx₂] at adj + exact h x₁ (G.adj_symm adj) hx₁ + · simp [hx₁, hx₂] + replace hx₁ : x₁ = v := mem_x₁.resolve_left hx₁ + simp [hx₁] at adj + -- TODO the following 2 lines are kind of cumbersome + intro wrong + exact (h x₂ adj hx₂) (Eq.symm wrong) + · intro a + simp_all only [comap_adj, Function.Embedding.coe_subtype] + simp_all only [Set.union_singleton, Set.mem_insert_iff, or_false, SimpleGraph.irrefl] + +lemma preimage_val_card {A B : Set V} : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by + apply Finset.card_bij' + case i => exact fun a _ => ↑a + case j => + intro a h + simp only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset] at h + exact ⟨a, h.left⟩ + case hi => + intro a ha + simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage, Set.toFinset_inter, + Finset.mem_inter, Subtype.coe_prop, and_self] + case hj => + intro a ha + simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage] + simp_all only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset] + case left_inv => + intro a ha + simp_all only [not_false_eq_true, true_and, Subtype.coe_eta] + case right_inv => + intro a ha + simp_all only [not_false_eq_true, true_and] + +theorem color_path + (k : ℕ) (maxDeg_le_k : G.maxDegree ≤ k) + {u v : V} (P : G.Path u v) + (S : Set V) + (P_outside_S : ∀ x ∈ P.val.support, x ∉ S) + (S_colorable : Colorable (G.induce S) k) + : Colorable (G.induce (S ∪ P.val.support.tail.toSet)) k := by + classical + let ⟨W, W_is_path⟩ := P + cases W with + | nil => + simp + rw [List.toSet_nil, Set.union_empty] + exact S_colorable + | @cons u w v adj W' => + simp at * + let P' : G.Path w v := ⟨W', IsPath.of_cons W_is_path⟩ + have P'_colorable := color_path k maxDeg_le_k P' S (P_outside_S.right) S_colorable + let P'_coloring := P'_colorable.some + + let N := G.neighborSet w + -- set of vertices already colored by P'_coloring + let C := S ∪ W'.support.tail.toSet + + have u_not_in_W' : u ∉ W'.support := ((Walk.cons_isPath_iff adj W').mp W_is_path).right + have u_not_in_W'_tail : u ∉ W'.support.tail := by + intro wrong + have u_in_W' := List.Mem.tail w wrong + rw [←(Walk.support_eq_cons W')] at u_in_W' + contradiction + have hu : u ∈ (N \ C) := by + simp [N, C] + exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩ + + have card_fact : (C ↓∩ N).toFinset.card = (C ∩ N).toFinset.card := + -- TODO the below gives a timeout error + -- preimage_val_card + sorry + + have unused_color : ∃ c : Fin k, c ∉ P'_coloring '' (C ↓∩ N) := by + suffices (P'_coloring '' (C ↓∩ N)).toFinset.card < (Set.univ : Set (Fin k)).toFinset.card from by + have ⟨c, hc⟩ := Finset.exists_mem_not_mem_of_card_lt_card this + simp only [Set.mem_toFinset] at hc + exact ⟨c, hc.right⟩ + simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin] + suffices (C ↓∩ N).toFinset.card < k from calc + (Finset.image (⇑P'_coloring) (C ↓∩ N).toFinset).card ≤ (C ↓∩ N).toFinset.card := Finset.card_image_le + _ < k := this + have ineq1 : (C ↓∩ N).toFinset.card + (N \ C).toFinset.card ≤ k := calc + (C ↓∩ N).toFinset.card + (N \ C).toFinset.card = (N ∩ C).toFinset.card + (N \ C).toFinset.card := by simp only [card_fact, Set.inter_comm] + _ = N.toFinset.card := by simp only [Set.toFinset_inter, Set.toFinset_diff, Finset.card_inter_add_card_sdiff] + _ ≤ G.maxDegree := G.degree_le_maxDegree w + _ ≤ k := maxDeg_le_k + have ineq2 : 1 ≤ (N \ C).toFinset.card := by + simp only [Finset.one_le_card, Set.toFinset_nonempty] + exact ⟨u, hu⟩ + linarith + + let ⟨c, hc⟩ := unused_color + have extended_coloring := extend_coloring G (S ∪ W'.support.tail.toSet) P'_coloring w c hc + + have fact : (W'.support.tail.toSet ∪ {w} : Set V) = W'.support.toSet := by + simp [List.toSet, Set.union_def, Or.comm, Walk.mem_support_iff] + + rw [Set.union_assoc, fact] at extended_coloring + exact Nonempty.intro extended_coloring + +-- lemma trivial_graph_colorable {k : ℕ} (h : Fintype.card V = 0) : Colorable G k := by +-- simp [Fintype.card_eq_zero_iff, IsEmpty] at h +-- apply Nonempty.intro +-- apply Coloring.mk +-- case color => exact isEmptyElim +-- case valid => +-- intro v +-- exact isEmptyElim v + +namespace SimpleGraph + theorem maxDegree_mono (G' : Subgraph G) : G'.maxDegree ≤ G.maxDegree := by + apply maxDegree_le_of_forall_degree_le + intro v + calc + G'.degree v + +theorem brooks' + (k : ℕ) (k_ge_3 : k ≥ 3) + (maxDeg_le_k : G.maxDegree ≤ k) + (no_max_clique : CliqueFree G (k + 1)) + : Colorable G k := by + induction hn : Fintype.card V using Nat.strong_induction_on generalizing V G + case h n ih _ => + by_cases h : n ≤ k + · have n_colorable := G.colorable_of_fintype + rw [hn] at n_colorable + exact Colorable.mono h n_colorable + · by_cases k_reg : G.IsRegularOfDegree k + case neg => + simp [IsRegularOfDegree] at k_reg + have ⟨x, hx⟩ := k_reg + let S : Set V := Set.univ \ {x} + let G' := G.induce S + have S_maxDeg_le_k : G'.maxDegree ≤ k := G. + case pos => sorry diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..76f1718 --- /dev/null +++ b/flake.lock @@ -0,0 +1,113 @@ +{ + "nodes": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1743550720, + "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "c621e8422220273271f52058f618c94e405bb0f5", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-parts_2": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib_2" + }, + "locked": { + "lastModified": 1727826117, + "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "lean4-nix": { + "inputs": { + "flake-parts": "flake-parts_2", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1743534244, + "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=", + "owner": "lenianiva", + "repo": "lean4-nix", + "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d", + "type": "github" + }, + "original": { + "owner": "lenianiva", + "repo": "lean4-nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1743583204, + "narHash": "sha256-F7n4+KOIfWrwoQjXrL2wD9RhFYLs2/GGe/MQY1sSdlE=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "2c8d3f48d33929642c1c12cd243df4cc7d2ce434", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1743296961, + "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "nixpkgs-lib_2": { + "locked": { + "lastModified": 1727825735, + "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz" + } + }, + "root": { + "inputs": { + "flake-parts": "flake-parts", + "lean4-nix": "lean4-nix", + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..ac2e3a4 --- /dev/null +++ b/flake.nix @@ -0,0 +1,50 @@ +{ + description = "Lean 4 Example Project"; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + flake-parts.url = "github:hercules-ci/flake-parts"; + lean4-nix = { + url = "github:lenianiva/lean4-nix"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + }; + + outputs = inputs @ { + nixpkgs, + flake-parts, + lean4-nix, + ... + }: + flake-parts.lib.mkFlake {inherit inputs;} { + systems = [ + "aarch64-darwin" + "aarch64-linux" + "x86_64-darwin" + "x86_64-linux" + ]; + + perSystem = { + system, + pkgs, + ... + }: { + _module.args.pkgs = import nixpkgs { + inherit system; + overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; + }; + + packages.default = + (pkgs.lean.buildLeanPackage { + name = "Example"; + roots = ["Main"]; + src = pkgs.lib.cleanSource ./.; + }) + .executable; + + devShells.default = pkgs.mkShell { + packages = with pkgs.lean; [lean lean-all]; + }; + }; + }; +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..e3283a2 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "aa936c36e8484abd300577139faf8e945850831a", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.18.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.53", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ecaaeb0b44a8d5784f17bd417e83f44c906804ab", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0e05c2f090b7dd7a2f530bdc48a26b546f4837c7", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "613510345e4d4b3ce3d8c129595e7241990d5b39", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "brooks", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..137e7f4 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "brooks" +defaultTargets = ["Brooks"] + +[[lean_lib]] +name = "Brooks" + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.18.0" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..8259911 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.18.0 \ No newline at end of file |