Interval Set

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

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

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

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

theorem NonemptyInterval.ext {α : Type} {inst✝ : LE α} {x y : NonemptyInterval α} (toProd : x.toProd = y.toProd) : x = y

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

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 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 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 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 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₁ 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 b : Char} : Interval.Char.sub a b = a - b

def Interval.between (r1 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 [] = (true = true)
• Intervals.dataIsNonOverlapping [head] = (true = true)
• Intervals.dataIsNonOverlapping (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.toList

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

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

• Interval.nonOverlappingWithLast intervals (some next_2) = Interval.nonOverlapping last next_2
• Interval.nonOverlappingWithLast intervals (some val) = (true = true)
• Interval.nonOverlappingWithLast intervals none = (true = true)
• Interval.nonOverlappingWithLast intervals none = (false = true)

structure Interval.Acc : Type

Accumulator for loop in canonicalize

• next : Option (NonemptyInterval Char)
• set : IntervalSet Char
• nonOverlapping : 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 (some next_2) n = (next_2.fst = n.fst)
• Interval.is_start_eq next n = (true = true)