import Mathlib

set_option autoImplicit false

namespace MM

def Y443Arms : Fin 3 → ℕ
  | ⟨0, _⟩ => 4
  | ⟨1, _⟩ => 4
  | ⟨_, _⟩ => 3

theorem Y443Arms_pos (i : Fin 3) : 0 < Y443Arms i := by fin_cases i <;> decide

def Y443Vertex : Type := Unit ⊕ Σ i : Fin 3, Fin (Y443Arms i)

instance : Fintype Y443Vertex := inferInstanceAs (Fintype (Unit ⊕ Σ i : Fin 3, Fin (Y443Arms i)))
instance : DecidableEq Y443Vertex :=
  inferInstanceAs (DecidableEq (Unit ⊕ Σ i : Fin 3, Fin (Y443Arms i)))

namespace Y443Vertex
def torso : Y443Vertex := Sum.inl ()
def arm (i : Fin 3) (v : Fin (Y443Arms i)) : Y443Vertex := Sum.inr ⟨i, v⟩
end Y443Vertex

open Y443Vertex

inductive Y443EdgeD : Y443Vertex → Y443Vertex → Prop where
  | torso (i : Fin 3) : Y443EdgeD torso (arm i ⟨0, Y443Arms_pos i⟩)
  | arm (i : Fin 3) (v : Fin (Y443Arms i)) (h : v.val + 1 < Y443Arms i) :
      Y443EdgeD (arm i v) (arm i ⟨v.val + 1, h⟩)

def Y443Edge (x y : Y443Vertex) : Prop := Y443EdgeD x y ∨ Y443EdgeD y x

theorem Y443EdgeD_ne {x y : Y443Vertex} (h : Y443EdgeD x y) : x ≠ y := by
  intro hxy; subst hxy
  cases h with
  | torso i => simp [torso, arm]
  | arm i v hv => simp at hv

theorem Y443Edge_ne {x y : Y443Vertex} (h : Y443Edge x y) : x ≠ y := fun hxy =>
  h.elim (fun h1 => Y443EdgeD_ne h1 hxy) (fun h2 => Y443EdgeD_ne h2 hxy.symm)

theorem Y443Edge_symm {x y : Y443Vertex} (h : Y443Edge x y) : Y443Edge y x := h.symm

theorem Y443Edge_irrefl (x : Y443Vertex) : ¬ Y443Edge x x := fun h => Y443Edge_ne h rfl

-- decidability, proved by analysis rather than by unfolding
instance : DecidableRel Y443EdgeD := fun x y => by
  revert x y
  intro x y
  refine match x, y with
    | torso, torso => isFalse (by intro h; cases h)
    | torso, arm i v =>
        if hv : v.val = 0 then isTrue ?_ else isFalse ?_
    | arm i v, torso => isFalse (by intro h; cases h)
    | arm i v, arm j w =>
        if hij : i = j then
          if hw : w.val = v.val + 1 then isTrue ?_ else isFalse ?_
        else isFalse ?_
  · exact hv ▸ Y443EdgeD.torso i
  · intro h; cases h with | torso j => simp at hv
  · subst hij
    have hlt : v.val + 1 < Y443Arms i := by
      have := w.isLt; omega
    have : w = ⟨v.val + 1, hlt⟩ := Fin.ext (by simp [hw])
    exact this ▸ Y443EdgeD.arm i v hlt
  · intro h; cases h with | arm _ _ _ => simp_all
  · intro h; cases h with | arm _ _ _ => simp_all

instance : DecidableRel Y443Edge := fun x y =>
  inferInstanceAs (Decidable (Y443EdgeD x y ∨ Y443EdgeD y x))

example : Fintype.card Y443Vertex = 12 := by
  show Fintype.card (Unit ⊕ Σ i : Fin 3, Fin (Y443Arms i)) = 12
  rw [Fintype.card_sum, Fintype.card_sigma]
  decide

def Y443Entry (x y : Y443Vertex) : ℕ :=
  if x = y then 1 else if Y443Edge x y then 3 else 2

def Y443Matrix : CoxeterMatrix Y443Vertex where
  M := Matrix.of Y443Entry
  isSymm := Matrix.IsSymm.ext fun i j => by
    show Y443Entry j i = Y443Entry i j
    by_cases h : i = j
    · subst h; rfl
    · rw [if_neg (Ne.symm h), if_neg h]
      by_cases he : Y443Edge i j
      · rw [if_pos he, if_pos (Y443Edge_symm he)]
      · rw [if_neg he, if_neg (fun hc => he (Y443Edge_symm hc))]
  diagonal := fun i => by
    show Y443Entry i i = 1
    rw [if_pos rfl]

@[simp] theorem Y443Matrix_apply (i j : Y443Vertex) : Y443Matrix.M i j = Y443Entry i j :=
  Matrix.of_apply ..

-- the decisive counting test: all 144 entries
example :
    (Finset.univ.val.map (fun p : Y443Vertex × Y443Vertex => Y443Matrix.M p.1 p.2)) =
      (Multiset.replicate 12 1 + Multiset.replicate 22 3 + Multiset.replicate 110 2 :
        Multiset ℕ) := by
  decide

end MM
