optimal schedules

Stream: Is there code for X?

[Frederick Pu]

Is there any code related to optimal schedules written in lean. If not here's a brief write up:
We define an interval to be tuple of real number (start, end) where start <= end
Two intervals intersect iff the intersection of their underlying sets (fun (start, end) => Set.Ioo start, end) is nonempty. In particular intervals (0, 1) (1, 2) are not considered to be intersecting.

Given a list of intervals l : List (Real x Real), a schedule on l is a sublist of l such that for any two distinct intervals (intervals at different indexes in the list) they are not intersecting. An optimal schedule g on a list l : List (Real x Real) is the schedule on l with the maximal possible length (all other schedules on l will have at most length g.length). Note that there can be multiple optimal schedules but they will have the same length.

The main goal for optimal schedules would be to prove that following program always returns the optimal schedule

def optimalSchedule(intervals):
         intervals = intervals.sort()
         S = []
         f = -inf
         for i in range(n):
                  if start[i] >= f:
                             S.append([start[i], end[i]])
                             f = end[i]
         return S

[Yaël Dillies]

Some people were interested in this back in september, but I haven't heard back from them. So I would assume "No, there is no code on optimal scheduling" :smile:

[Frederick Pu]

i wrote an informal proof for it and it mainly boils down to a very nasty lemma:

Let $G$ be an optimal schedule on $intervals$ and $f$ be $-inf$ or a real number such that $\{[start, end] \in G, end \geq f \}$ is nonempty.
Define $[start_b, end_b]$, to be an element in $\{[start, end] \in G, end \geq f \wedge start \neq end \}$ with the smallest end point.
For any $[start, end] \in intervals$ such that $end \leq end_b$ and $start \geq f$,
defining $G'$ to be the list formed by replacing $[start_b, end_b]$ with $[start, end]$ in $G$, $G'$ is an optimal schedule of intervals.

[Frederick Pu]

how do i format latex in zulip lol

[Yaël Dillies]

Two $$, not just one

[Daniel Weber]

It could be interesting to more generally formalize chordal graphs