theorem Intervals.empty_isNonOverlapping {α : Type} [LE α] [HSub α α Nat] : nonOverlapping #[]

theorem Intervals.single_isNonOverlapping (ranges : Array (NonemptyInterval Char)) (h : ranges.size = 1) : nonOverlapping ranges

instance Intervals.instInhabitedIntervalSet (α : Type) [LT α] [LE α] [HSub α α Nat] [(a b : α) → Decidable (a < b)] [(a b : α) → Decidable (a = b)] : Inhabited (IntervalSet α)

Equations

• Intervals.instInhabitedIntervalSet α = { default := { intervals := #[], isNonOverlapping := ⋯ } }

def Intervals.singleton (r : NonemptyInterval Char) : IntervalSet Char

Equations

• Intervals.singleton r = { intervals := #[r], isNonOverlapping := ⋯ }

theorem Intervals.pred_lt' {n m : Nat} (h : m < n) : n.pred < n

theorem Intervals.Fin.pred {n : Nat} {i : Fin n} (h : 0 < ↑i) : ↑i - 1 < n

theorem Intervals.isNonOverlapping (l r : NonemptyInterval Char) (h1 : ¬r.fst.toNat - l.snd.toNat = 1) (h2 : ¬r.fst < l.snd) (h3 : ¬l.snd = r.fst) : Interval.nonOverlapping l r

theorem Intervals.nonOverlappingWithLast_of_empty (ranges : Array (NonemptyInterval Char)) (next : Option (NonemptyInterval Char)) (h2 : ranges.size = 0) : Interval.nonOverlappingWithLast ranges next

theorem Intervals.nonOverlappingWithLast_with_none_eq_empty (acc : Interval.Acc) (h : acc.next.isNone = true) : acc.set.intervals.size = 0

theorem Intervals.nonOverlappingWithLast_of_none (acc : Interval.Acc) (n : NonemptyInterval Char) (h : acc.next.isNone = true) : Interval.nonOverlappingWithLast acc.set.intervals (some n)

theorem Intervals.nonOverlappingWithLast_of_val (acc : Interval.Acc) (n : NonemptyInterval Char) (h : Interval.is_start_eq acc.next n) : Interval.nonOverlappingWithLast acc.set.intervals (some n)

theorem Intervals.is_start_eq_of_val {l : NonemptyInterval Char} (next : Option (NonemptyInterval Char)) (n : NonemptyInterval Char) (hm : next = some l) (hx : l.fst = n.fst) : Interval.is_start_eq next n

theorem Intervals.is_start_eq_of_none (next : Option (NonemptyInterval Char)) (n : NonemptyInterval Char) (hm : next = none) : Interval.is_start_eq next n

theorem Intervals.nonOverlappingWithLast_of_singleton (l r : NonemptyInterval Char) (h : Interval.nonOverlapping l r) : Interval.nonOverlappingWithLast (singleton l).intervals (some r)

theorem Intervals.nonOverlapping_of_push {last : NonemptyInterval Char} (acc : Interval.Acc) (next : NonemptyInterval Char) (h1 : acc.set.intervals.last? = some last) (h2 : acc.next = some next) : nonOverlapping (acc.set.intervals.push next)

theorem Intervals.List.eq_head_of_get_first {α : Type u_1} {head : α} {tail : List α} (arr : List α) (h1 : 0 < arr.length) (h2 : arr = head :: tail) : head = arr.get ⟨0, h1⟩

theorem Intervals.Array.eq_head_of_get_first {α : Type u_1} {head : α} {tail : List α} (arr : Array α) (h1 : 0 < arr.size) (h2 : arr.toList = head :: tail) : head = arr[0]

theorem Intervals.nonOverlapping_of_nth {head : NonemptyInterval Char} {tail : List (NonemptyInterval Char)} (ranges : Array (NonemptyInterval Char)) (n : Nat) (h1 : 0 < n) (h2 : n + 1 < ranges.size) (h3 : ranges.toList = head :: tail) (h4 : ∀ (i : Nat) (h : i < tail.length - 1), Interval.nonOverlapping (tail.get ⟨i, ⋯⟩) (tail.get ⟨i + 1, ⋯⟩)) : Interval.nonOverlapping ranges[n] ranges[n + 1]

theorem Intervals.nonOverlapping_of_pred (ranges : Array (NonemptyInterval Char)) (i : Fin ranges.size) (x y : NonemptyInterval Char) (h : 0 < ↑i) (hx : x = ranges[↑i - 1]) (hy : y = ranges[↑i]) (hr : nonOverlapping ranges) : Interval.nonOverlapping x y

theorem Intervals.nonOverlappingWithLast_of_push {l r : NonemptyInterval Char} (acc : Interval.Acc) (h2 : nonOverlapping (acc.set.intervals.push l)) (h3 : Interval.nonOverlapping l r) : Interval.nonOverlappingWithLast (acc.push l h2).intervals (some r)