-- File: lean/PathSpec.lean
-- Path Canonicalization Specification
-- Agents migrate a C path library to Rust (Vec<String> segment lists).
-- Path = List String where each element is a non-empty segment (no "/" markers).

namespace PathSpec

abbrev Path := List String

-- Internal: reversed accumulator, head = most recently added segment
def normalizeAux (acc : Path) : Path → Path
  | [] => acc.reverse
  | seg :: rest =>
    if seg == "." then normalizeAux acc rest
    else if seg == ".." then
      match acc with
      | [] => normalizeAux [] rest        -- clamp at root
      | _ :: acc' => normalizeAux acc' rest
    else normalizeAux (seg :: acc) rest

-- Remove "." segments; resolve ".." clamped at root
def normalize (p : Path) : Path := normalizeAux [] p

-- Join two segment lists: normalize the concatenation
def join (base rel : Path) : Path := normalize (base ++ rel)

-- Path depth = segment count
def depth (p : Path) : Nat := p.length

-- A path is in normal form if it contains no "." or ".." segments
def isNormal (p : Path) : Bool :=
  p.all (fun s => s != "." && s != "..")

-- Helper: elements of normalizeAux output are never "." or ".."
theorem normalizeAux_no_special (acc p : Path)
    (hacc : ∀ s ∈ acc, s ≠ "." ∧ s ≠ "..") :
    ∀ s ∈ normalizeAux acc p, s ≠ "." ∧ s ≠ ".." := by
  induction p generalizing acc with
  | nil =>
    intro s hs
    simp only [normalizeAux] at hs
    exact hacc s (List.mem_reverse.mp hs)
  | cons seg rest ih =>
    intro s hs
    cases h1 : (seg == ".")
    · -- (seg == ".") = false
      cases h2 : (seg == "..")
      · -- (seg == "..") = false — seg is normal, pushed onto acc
        simp only [normalizeAux, h1, h2] at hs
        apply ih (seg :: acc) _ s hs
        intro t ht
        rcases List.mem_cons.mp ht with rfl | ht'
        · exact ⟨fun heq => by simp [heq] at h1, fun heq => by simp [heq] at h2⟩
        · exact hacc t ht'
      · -- (seg == "..") = true — pop acc
        cases acc with
        | nil =>
          simp only [normalizeAux, h1, h2, ↓reduceIte] at hs
          exact ih [] (fun _ hm => by simp at hm) s hs
        | cons x acc' =>
          simp only [normalizeAux, h1, h2, ↓reduceIte] at hs
          exact ih acc' (fun t ht => hacc t (List.mem_cons.mpr (Or.inr ht))) s hs
    · -- (seg == ".") = true — skip
      simp only [normalizeAux, h1, ↓reduceIte] at hs
      exact ih acc hacc s hs

-- Helper: normalizeAux on a path with no special segments equals acc.reverse ++ p
theorem normalizeAux_on_normal (acc p : Path)
    (hp : ∀ s ∈ p, s ≠ "." ∧ s ≠ "..") :
    normalizeAux acc p = acc.reverse ++ p := by
  induction p generalizing acc with
  | nil => simp [normalizeAux]
  | cons seg rest ih =>
    obtain ⟨hne1, hne2⟩ := hp seg (List.mem_cons.mpr (Or.inl rfl))
    have h1 : (seg == ".") = false := beq_eq_false_iff_ne.mpr hne1
    have h2 : (seg == "..") = false := beq_eq_false_iff_ne.mpr hne2
    simp only [normalizeAux, h1, h2]
    rw [ih (seg :: acc) (fun s hs => hp s (List.mem_cons.mpr (Or.inr hs)))]
    simp [List.reverse_cons, List.append_assoc]

-- Normalization is idempotent
theorem normalize_idempotent (p : Path) : normalize (normalize p) = normalize p := by
  unfold normalize
  rw [normalizeAux_on_normal []
    (normalizeAux [] p)
    (normalizeAux_no_special [] p (fun _ h => by simp at h))]
  simp

-- DRT checks (native_decide: ground equalities)
example : normalize ["usr", "local", "..", "bin"] = ["usr", "bin"] := by native_decide
example : normalize [".", "a", ".", "b"] = ["a", "b"] := by native_decide
example : normalize ["..", "a"] = ["a"] := by native_decide
example : normalize ["a", "b", "..", ".."] = [] := by native_decide
example : normalize ["a", ".", "b", "..", "c"] = ["a", "c"] := by native_decide
example : join ["usr", "local"] ["bin"] = ["usr", "local", "bin"] := by native_decide
example : join ["a", "b"] [".."] = ["a"] := by native_decide
example : depth ["a", "b", "c"] = 3 := by native_decide
example : depth [] = 0 := by native_decide

end PathSpec