init main

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