Spaces:
Sleeping
Sleeping
File size: 2,543 Bytes
bf9c466 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 | -- 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
|