Interval Set

This file contains the definition of interval sets (IntervalSet), a sorted set of non-overlapping intervals (Interval.nonOverlapping).

theorem NonemptyInterval.ext {α : Type} : ∀ {inst : LE α} {x y : NonemptyInterval α}, x.toProd = y.toProd → x = y

theorem NonemptyInterval.ext_iff {α : Type} : ∀ {inst : LE α} {x y : NonemptyInterval α}, x = y ↔ x.toProd = y.toProd

structure NonemptyInterval (α : Type) [LE α] extends Prod : Type

• fst : α
• snd : α
• fst_le_snd : self.fst ≤ self.snd

  The starting point of an interval is smaller than the endpoint.

theorem NonemptyInterval.fst_le_snd {α : Type} [LE α] (self : NonemptyInterval α) : self.fst ≤ self.snd

The starting point of an interval is smaller than the endpoint.

class BoundedOrder (α : Type) [LE α] : Type

A bounded order describes an order (≤) with a top and bottom element, see Mathlib.Order.BoundedOrder

• bot : α
• bot_le : ∀ (a : α), BoundedOrder.bot ≤ a
• top : α
• le_top : ∀ (a : α), a ≤ BoundedOrder.top

theorem BoundedOrder.bot_le {α : Type} [LE α] [self : BoundedOrder α] (a : α) : BoundedOrder.bot ≤ a

theorem BoundedOrder.le_top {α : Type} [LE α] [self : BoundedOrder α] (a : α) : a ≤ BoundedOrder.top

instance instBoundedOrderChar : BoundedOrder Char

BoundedOrder is used to define negation of interval sets (IntervalSet.negate).

Equations

• instBoundedOrderChar = { bot := Char.min, bot_le := Char.min_le, top := Char.max, le_top := Char.le_max }

theorem NonemptyInterval.eq_val_of_eq {α : Type} [LE α] {x : NonemptyInterval α} {y : NonemptyInterval α} (h : x = y) : x.fst = y.fst ∧ x.snd = y.snd

instance instDecidableEqNonemptyInterval (α : Type) [LE α] [DecidableEq α] : DecidableEq (NonemptyInterval α)

Equations

• One or more equations did not get rendered due to their size.

instance instToStringNonemptyIntervalChar : ToString (NonemptyInterval Char)

Equations

• instToStringNonemptyIntervalChar = { toString := fun (s : NonemptyInterval Char) => toString "" ++ toString s.fst ++ toString " " ++ toString s.snd ++ toString "" }

instance instInhabitedNonemptyIntervalChar : Inhabited (NonemptyInterval Char)

Equations

• instInhabitedNonemptyIntervalChar = { default := { toProd := default, fst_le_snd := instInhabitedNonemptyIntervalChar.proof_1 } }

def Interval.nonOverlapping {α : Type} [LE α] [HSub α α Nat] (r1 : NonemptyInterval α) (r2 : NonemptyInterval α) : Prop

Nonempty intervals r1 and r2 are non overlapping when they are sorted and they are not overlapping or adjacent, i.e. the difference of r2.fst and r1.snd is greater than one. Intervals with a difference of one are canonicalized to a new NonemptyInterval (IntervalSet.canonicalize).

Equations

• Interval.nonOverlapping r1 r2 = (1 < r2.fst - r1.snd)

instance Interval.instDecidableNonOverlapping {α : Type} [LE α] [HSub α α Nat] (r1 : NonemptyInterval α) (r2 : NonemptyInterval α) : Decidable (Interval.nonOverlapping r1 r2)

Equations

• Interval.instDecidableNonOverlapping r1 r2 = inferInstanceAs (Decidable (1 < r2.fst - r1.snd))

def Interval.intersection {α : Type} [LE α] [(a b : α) → Decidable (a ≤ b)] (r1 : NonemptyInterval α) (r2 : NonemptyInterval α) : Option (NonemptyInterval α)

create intersection of intervals r1 and r2 if it exists.

Equations

• One or more equations did not get rendered due to their size.

def Interval.Char.sub (c₁ : Char) (c₂ : Char) : Nat

Equations

• Interval.Char.sub c₁ c₂ = c₁.toNat - c₂.toNat

instance Interval.instHSubCharNat_regex : HSub Char Char Nat

Equations

• Interval.instHSubCharNat_regex = { hSub := Interval.Char.sub }

theorem Interval.Char.sub_def {a : Char} {b : Char} : Interval.Char.sub a b = a - b

def Interval.between (r1 : NonemptyInterval Char) (r2 : NonemptyInterval Char) (h : Interval.nonOverlapping r1 r2) : NonemptyInterval Char

create interval between intervals r1 and r2.

Equations

• Interval.between r1 r2 h = { toProd := (r1.snd.increment, r2.fst.decrement), fst_le_snd := ⋯ }

def Intervals.unique (intervals : Array (NonemptyInterval Char)) : Array (NonemptyInterval Char)

remove duplicate

Equations

• One or more equations did not get rendered due to their size.

def Intervals.dataIsNonOverlapping {α : Type} [LE α] [HSub α α Nat] (intervals : List (NonemptyInterval α)) : Prop

a list of intervals is non overlapping when intervals are sorted and no intervals are overlapping or adjacent

Equations

• Intervals.dataIsNonOverlapping intervals = match intervals with | [] => true = true | [head] => true = true | head :: tail => List.Chain Interval.nonOverlapping head tail

def Intervals.nonOverlapping {α : Type} [LE α] [HSub α α Nat] (intervals : Array (NonemptyInterval α)) : Prop

an array of intervals is non overlapping when intervals.data is non overlapping

Equations

• Intervals.nonOverlapping intervals = Intervals.dataIsNonOverlapping intervals.data

structure IntervalSet (α : Type) [LT α] [LE α] [HSub α α Nat] [(a b : α) → Decidable (a < b)] [(a b : α) → Decidable (a = b)] : Type

A sorted set of non-overlapping intervals.

• intervals : Array (NonemptyInterval α)
• isNonOverlapping : Intervals.nonOverlapping self.intervals

theorem IntervalSet.isNonOverlapping {α : Type} [LT α] [LE α] [HSub α α Nat] [(a b : α) → Decidable (a < b)] [(a b : α) → Decidable (a = b)] (self : IntervalSet α) : Intervals.nonOverlapping self.intervals

instance instToStringIntervalSetChar : ToString (IntervalSet Char)

Equations

• instToStringIntervalSetChar = { toString := fun (s : IntervalSet Char) => toString "" ++ toString s.intervals ++ toString "" }

def Interval.nonOverlappingWithLast (intervals : Array (NonemptyInterval Char)) (next : Option (NonemptyInterval Char)) : Prop

last element of array intervals is non overlapping with NonemptyInterval next

Equations

• One or more equations did not get rendered due to their size.

structure Interval.Acc : Type

Accumulator for loop in canonicalize

• next : Option (NonemptyInterval Char)
• set : IntervalSet Char
• nonOverlapping : Interval.nonOverlappingWithLast self.set.intervals self.next

theorem Interval.Acc.nonOverlapping (self : Interval.Acc) : Interval.nonOverlappingWithLast self.set.intervals self.next

def Interval.Acc.push (acc : Interval.Acc) (next : NonemptyInterval Char) (h : Intervals.nonOverlapping (acc.set.intervals.push next)) : IntervalSet Char

Equations

• acc.push next h = { intervals := acc.set.intervals.push next, isNonOverlapping := h }

def Interval.is_start_eq (next : Option (NonemptyInterval Char)) (n : NonemptyInterval Char) : Prop

is next.fst equal to n.fst

Equations

• Interval.is_start_eq next n = match next with | some next => next.fst = n.fst | x => true = true