aoc2025_day01_part01.lean

structure Cursor where
  state: Nat
  size: Nat
  deriving Repr, DecidableEq

structure Line where
  offset: Int
  deriving Repr, DecidableEq

def Cursor.moveState (offset : Int) (cursor : Cursor) : Cursor :=
  let size : Int := cursor.size
  let state : Int := cursor.state
  let newState := (state + offset) % size
  { cursor with state := newState.toNat }

example : (Cursor.moveState 2 { size := 5, state := 2 }) = { size := 5, state := 4 } := by native_decide

example : (Cursor.moveState 0 { state := 0, size := 1 }).state = 0 := by native_decide
theorem size_never_changes (start size offset : Nat)
  : (Cursor.moveState offset { size := size, state := start }).size = size
  := by rfl

theorem state_never_reaches_size (start : Nat) (size : Nat) (offset : Nat)
 (h₁ : size > 0)
 : (Cursor.moveState offset { size := size, state := start }).state < size
 := by
  apply Nat.mod_lt
  apply h₁

def parseLine (line : String) : Option Line :=
  (match line.toList with
  | 'R' :: rest => (String.ofList rest).toInt?
  | 'L' :: rest => (String.ofList rest).toInt?.map (· * -1)
  | _ => none).map ({ offset := · })

example : (parseLine "R2") = some { offset := 2 } := by native_decide

def foldCursor (cursor: Cursor) (lines: List Line) : List Cursor :=
  match lines with
  | [] => []
  | l :: r =>
    let new_cursor := cursor.moveState (l.offset)
    new_cursor :: foldCursor new_cursor r

def solve_part_1 (lines: List String) : Nat :=
  (((foldCursor ({ size := 100, state := 50 }) ((lines.filterMap parseLine)))).map (fun (x : Cursor) => x.state == 0)).count true