/-
Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Judith Ludwig, Christian Merten
-/
import BruhatTits.Graph.GroupAction

/-!
# Proof that the Bruhat-Tits graph is a tree

Let `R` be a discrete valuation ring and `K` its fraction field.

In this file we show that the Bruhat-Tits graph associated to `R` is acyclic (i.e. without loops)
and conclude that it is a tree. The connectedness was already shown in `BruhatTits.Graph.Graph`
(see `BruhatTits.BTGraph_connected`).

The strategy for proving acyclicity is as follows:

- Show that every trail (i.e. a walk that has no self-intersections in the interior, but possibly
  at the ends) can be transformed into a standard walk by the action of `GL₂(K)`. Here a standard
  walk is a walk that is represented by a standard sequence of lattices (see `List.IsStandard`).
- The length of a standard walk is the distance (in the sense of `inv`) of the endpoints, so
  by the first point, this also holds for every trail.
- In particular, the second point holds for a circle at `x`, but a circle always has length at least
  `3 > 0 = inv x x`, so no circles exist.

-/

namespace BruhatTits

variable {K : Type*} [Field K]
variable {R : Subring K} [IsDiscreteValuationRing R] [IsFractionRing R K]

section Action

/-- Any walk is representable by a chain of lattices. If the walk is a trail,
the chain is simple (see `BruhatTits.exists_repr_isSimpleChain_of_isTrail`). -/
lemma _root_.SimpleGraph.Walk.exists_repr_isChain {x y : Vertices R} (p : BTgraph.Walk x y) :
    ∃ (l : List (Lattice R)), l.IsChain ∧ l.map (fun L ↦ ⟦L⟧) = p.support := by
  induction' p using SimpleGraph.Walk.rec with x x y z hadj p ih
  · refine Quotient.inductionOn' x (fun L ↦ ?_)
    refine ⟨[L], singleton_isChain L, by simp⟩
  · obtain ⟨l, hchain, hl⟩ := ih
    have lnenil : l ≠ [] := by
      rintro rfl
      apply p.support_ne_nil
      simpa using hl.symm
    match l with
    | (L :: l) =>
    have hLy : ⟦L⟧ = y := by
      rw [p.support_eq_cons] at hl
      simp only [List.map_cons, List.cons.injEq] at hl
      exact hl.left
    subst hLy
    obtain ⟨M, rfl, hstd⟩ := exists_repr_isStandardNeighbour_of_isNeighbour L x hadj.symm
    refine ⟨M :: L :: l, ?_, ?_⟩
    · exact cons_isChain_of hchain hstd
    · simpa

/-- A non-empty chain of lattices defines a walk on the Bruhat-Tits graph. -/
def chainToWalk (l : List (Lattice R)) (hl : l ≠ []) (hc : l.IsChain) :
    BTgraph.Walk ⟦l.head hl⟧ ⟦l.getLast hl⟧ := match l with
  | [L] => SimpleGraph.Walk.nil' ⟦L⟧
  | L₁ :: L₂ :: l =>
      have p : BTgraph.Adj ⟦L₁⟧ ⟦L₂⟧ := by
        apply isNeighbour_of_isStandardNeighbour
        have := hc.isStandardNeighbour
        simp only [List.chain'_cons] at this
        exact this.left
      let q : BTgraph.Walk ⟦L₂⟧ ⟦(L₁ :: L₂ :: l).getLast hl⟧ :=
        chainToWalk (L₂ :: l) (by simp) (isChain_of_cons_isChain (List.cons_ne_nil L₂ l) hc)
      q.cons p

lemma isSimpleChain_of_isTrail_aux {x y : Vertices R} (p : BTgraph.Walk x y)
    (hp : p.IsTrail) (l : List (Lattice R)) (hl : l.map (fun L ↦ ⟦L⟧) = p.support) :
    (List.zipWith₃ (fun L₁ _ L₃ ↦ ¬ Lattice.IsSimilar R L₁ L₃) l l.tail l.tail.tail).Forall id := by
  match p, l with
  | .nil, [L] => simp [List.zipWith₃]
  | .cons _ .nil, [_, _] => simp [List.zipWith₃]
  | .cons adj (.cons adj' .nil), [M, L, Q] =>
      simp only [List.map_cons, List.map_nil, SimpleGraph.Walk.support_cons,
        SimpleGraph.Walk.support_nil, List.cons.injEq, and_true] at hl
      simp only [List.tail_cons, List.zipWith₃, List.forall_cons, id_eq, List.Forall, and_true]
      intro h
      have : (⟦M⟧ : Vertices R) = ⟦Q⟧ := by simpa
      simp only [SimpleGraph.Walk.cons_isTrail_iff, SimpleGraph.Walk.IsTrail.nil,
        SimpleGraph.Walk.edges_nil, List.not_mem_nil, not_false_eq_true, and_self,
        SimpleGraph.Walk.edges_cons, List.mem_singleton, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
        Prod.swap_prod_mk, and_true, not_or, not_and, true_and] at hp
      apply hp.right
      rw [← hl.left, ← hl.right.right]
      exact this
  | .cons adj (.cons adj' <| .cons adj'' q), (L₁ :: L₂ :: L₃ :: l) =>
      simp only [List.map_cons, SimpleGraph.Walk.support_cons, List.cons.injEq] at hl
      simp only [SimpleGraph.Walk.cons_isTrail_iff, SimpleGraph.Walk.edges_cons, List.mem_cons,
        Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, and_true, not_or, not_and] at hp
      simp only [List.tail_cons, List.zipWith₃, List.forall_cons, id_eq]
      refine ⟨?_, ?_⟩
      · intro h
        have h1 := hl.left
        subst h1
        have h2 := hl.right.left
        subst h2
        have h3 := hl.right.right.left
        subst h3
        have h' : (⟦L₁⟧ : Vertices R) = ⟦L₃⟧ := by
          apply Quotient.sound
          exact h
        tauto
      · apply isSimpleChain_of_isTrail_aux (.cons adj' <| .cons adj'' q)
        · simp
          tauto
        · simp
          tauto

/-- If `p` is a trail in the Bruhat-Tits graph, it is representable by
  a simple chain of lattices. -/
lemma exists_repr_isSimpleChain_of_isTrail {x y : Vertices R} (p : BTgraph.Walk x y)
    (hp : p.IsTrail) :
    ∃ (l : List (Lattice R)), l.IsSimpleChain ∧ l.map (fun L ↦ ⟦L⟧) = p.support := by
  obtain ⟨l, hl, heq⟩ := p.exists_repr_isChain
  refine ⟨l, ⟨hl, ?_⟩, heq⟩
  apply isSimpleChain_of_isTrail_aux p hp _ heq

/-- A walk on the Bruhat-Tits graph is a standard walk, if there exists a sequence
of representing lattices `(Lᵢ)` with `pᵢ = ⟦Lᵢ⟧` such that the sequence `(Lᵢ)` is
a standard sequence (see `List.IsStandard`). -/
def _root_.SimpleGraph.Walk.IsStandard {x y : Vertices R} (p : BTgraph.Walk x y) : Prop :=
  ∃ (l : List (Lattice R)), l.map (fun L ↦ ⟦L⟧) = p.support ∧ l.IsStandard

lemma isStandard_of_list_isStandard {x y : Vertices R} {p : BTgraph.Walk x y}
    (l : List (Lattice R)) (hleq : l.map (fun L ↦ ⟦L⟧) = p.support) (hl : l.IsStandard) :
    p.IsStandard := by
  use l

/-- If `p` is a standard walk from `x` to `y`, the length of `p` is the distance `inv x y`. -/
lemma length_eq_inv_of_isStandard {x y : Vertices R} {p : BTgraph.Walk x y} (h : p.IsStandard) :
    p.length = inv x y := by
  obtain ⟨l, hleq, hl⟩ := h
  have hlen := length_eq_dist_add_one_of_isStandard hl
  have : p.support.length = dist (l.head hl.ne_nil) (l.getLast hl.ne_nil) + 1 := by
    rw [← hleq]
    simpa
  simp only [SimpleGraph.Walk.length_support, add_left_inj] at this
  have : x = ⟦l.head hl.ne_nil⟧ := by
    match l with
    | L :: l =>
    rw [p.support_eq_cons, List.map_cons, List.cons.injEq] at hleq
    simpa using hleq.left.symm
  subst this
  have : y = ⟦l.getLast hl.ne_nil⟧ := by
    apply_fun List.reverse at hleq
    rw [← p.support_reverse, p.reverse.support_eq_cons] at hleq
    rw [← List.getLast_map (f := fun L ↦ ⟦L⟧), List.getLast_eq_head_reverse]
    simp_rw [hleq]
    · rfl
    · simpa using List.ne_nil_of_length_eq_add_one hlen
  subst this
  assumption

/-- Given two vertices and a trail `p` from `x` to `y`, there exists a `g : GL₂(K)`
such that `g • p` is a standard walk. -/
lemma exists_map_isStandard {x y : Vertices R} {p : BTgraph.Walk x y} (hp : p.IsTrail) :
    ∃ (g : GL (Fin 2) K), (p.map (g.toGraphIso (R := R))).IsStandard (R := R) := by
  obtain ⟨l, hlsimple, heq⟩ := exists_repr_isSimpleChain_of_isTrail p hp
  obtain ⟨g, hg⟩ := exists_trafo_to_isStandard l hlsimple
  use g
  refine isStandard_of_list_isStandard (g • l) ?_ hg
  simp only [List.smul_lattice_def, List.map_map, RelEmbedding.coe_toRelHom,
    RelIso.coe_toRelEmbedding, SimpleGraph.Walk.support_map]
  show List.map (fun L ↦ ⟦g • L⟧) l = _
  simp_rw [← smulGL_mk, ← Vertices.smul_def]
  show List.map ((fun x : Vertices R ↦ g • x) ∘ (fun L ↦ ⟦L⟧)) l = _
  rw [List.comp_map, heq]
  rfl

end Action

section Acyclic

/-- The length of a trail is equal to the distance of the endpoints. -/
lemma length_eq_inv {x y : Vertices R} {p : BTgraph.Walk x y} (hp : p.IsTrail) :
    p.length = inv x y := by
  -- transform chain to standard one by a graph isomorphism, then apply the result for
  -- standard walks
  obtain ⟨g, hg⟩ := exists_map_isStandard hp
  have : (p.map (g.toGraphIso (R := R)).toHom).length = inv (g • x) (g • y) :=
    length_eq_inv_of_isStandard hg
  simpa using this

/-- The graph-theoretic distance agrees with our constructed `inv` function. -/
lemma dist_BTgraph_eq_inv : (BTgraph (R := R)).dist = inv := by
  ext x y
  obtain ⟨p, hp, hlen⟩ := (BTgraph_connected (R := R)).exists_path_of_dist x y
  rw [← hlen, length_eq_inv hp.isTrail]

/-- The Bruhat-Tits graph has no loops, i.e. it is acyclic. -/
lemma BTgraph_isAcyclic : (BTgraph (R := R)).IsAcyclic := by
  -- suppose `c` is a circle
  intro x c h
  -- then `c` is a trail, but the length of such a chain is the distance
  -- of the endpoints, which yields a contradiction
  have : c.length = inv x x := length_eq_inv h.isCircuit.isTrail
  rw [inv_self] at this
  have : 3 ≤ 0 := by
    rw [← this]
    exact SimpleGraph.Walk.IsCycle.three_le_length h
  contradiction

end Acyclic

/-- The Bruhat-Tits graph is a tree. -/
theorem BTtree : SimpleGraph.IsTree (BTgraph (R := R)) where
  isConnected := BTgraph_connected
  IsAcyclic := BTgraph_isAcyclic