-- File: lean/IntervalSpec.lean
-- Interval Scheduler Specification
-- Agents migrate a C++ interval merger + greedy scheduler to Rust.
-- Interval = (Int × Int), representing [start, end].

namespace IntervalSpec

abbrev Interval := Int × Int

-- Insertion sort by a key function (for deterministic ordering)
def insertBy (lt : Interval → Interval → Bool) (iv : Interval)
    : List Interval → List Interval
  | [] => [iv]
  | x :: rest =>
    if lt iv x then iv :: x :: rest
    else x :: insertBy lt iv rest

def sortBy (lt : Interval → Interval → Bool) (ivs : List Interval) : List Interval :=
  ivs.foldl (fun sorted iv => insertBy lt iv sorted) []

-- Drop last element from a list
def dropLast : List Interval → List Interval
  | [] => []
  | [_] => []
  | x :: rest => x :: dropLast rest

-- Merge overlapping or touching intervals (start ≤ previous end = merge)
def mergeIntervals (ivs : List Interval) : List Interval :=
  (sortBy (fun a b => a.1 < b.1) ivs).foldl (fun acc iv =>
    match acc.getLast? with
    | none => [iv]
    | some (ls, le) =>
      if iv.1 ≤ le then dropLast acc ++ [(ls, max le iv.2)]
      else acc ++ [iv]) []

-- Greedy activity selection: sort by end time, pick non-overlapping
def maxSchedule (ivs : List Interval) : List Interval :=
  (sortBy (fun a b => a.2 < b.2) ivs).foldl (fun acc iv =>
    match acc.getLast? with
    | none => [iv]
    | some (_, le) =>
      if le ≤ iv.1 then acc ++ [iv]
      else acc) []

-- Helper predicates for correctness theorems
def isSorted (ivs : List Interval) : Bool :=
  match ivs with
  | [] | [_] => true
  | (_, e1) :: (s2, e2) :: rest =>
    e1 ≤ s2 && isSorted ((s2, e2) :: rest)

def noOverlap (ivs : List Interval) : Bool :=
  match ivs with
  | [] | [_] => true
  | (_, e1) :: (s2, e2) :: rest =>
    e1 ≤ s2 && noOverlap ((s2, e2) :: rest)

-- mergeIntervals output is sorted and non-overlapping
theorem merge_sorted (ivs : List Interval) :
    isSorted (mergeIntervals ivs) = true := by
  sorry

theorem merge_no_overlap (ivs : List Interval) :
    noOverlap (mergeIntervals ivs) = true := by
  sorry

-- DRT checks
example : mergeIntervals [(1, 3), (2, 5), (7, 9)] = [(1, 5), (7, 9)] := by native_decide
example : mergeIntervals [(1, 4), (4, 6)] = [(1, 6)] := by native_decide
example : mergeIntervals [] = [] := by native_decide
example : maxSchedule [(1, 3), (2, 4), (3, 5)] = [(1, 3), (3, 5)] := by native_decide
example : maxSchedule [(1, 2), (3, 4), (5, 6)] = [(1, 2), (3, 4), (5, 6)] := by native_decide

end IntervalSpec