def Std.Time.Internal.Bounded (rel : Int → Int → Prop) (lo hi : Int) : Type

A Bounded is represented by an Int that is constrained by a lower and higher bounded using some relation rel. It includes all the integers that rel lo val ∧ rel val hi.

Equations

• Std.Time.Internal.Bounded rel lo hi = { val : Int // rel lo val ∧ rel val hi }

Instances For

• Std.Time.Internal.Bounded.instBEq
• Std.Time.Internal.Bounded.instLE
• Std.Time.Internal.Bounded.instLT
• Std.Time.Internal.Bounded.instRepr

@[always_inline]

instance Std.Time.Internal.Bounded.instLE {rel : Int → Int → Prop} {n m : Int} : _root_.LE (Bounded rel n m)

Equations

• Std.Time.Internal.Bounded.instLE = { le := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val ≤ r.val }

@[always_inline]

instance Std.Time.Internal.Bounded.instLT {rel : Int → Int → Prop} {n m : Int} : _root_.LT (Bounded rel n m)

Equations

• Std.Time.Internal.Bounded.instLT = { lt := fun (l r : Std.Time.Internal.Bounded rel n m) => l.val < r.val }

@[always_inline]

instance Std.Time.Internal.Bounded.instRepr {rel : Int → Int → Prop} {m n : Int} : Repr (Bounded rel m n)

Equations

• Std.Time.Internal.Bounded.instRepr = { reprPrec := fun (n_1 : Std.Time.Internal.Bounded rel m n) => reprPrec n_1.val }

@[always_inline]

instance Std.Time.Internal.Bounded.instBEq {rel : Int → Int → Prop} {n m : Int} : BEq (Bounded rel n m)

Equations

• Std.Time.Internal.Bounded.instBEq = { beq := fun (x y : Std.Time.Internal.Bounded rel n m) => decide (x.val = y.val) }

@[always_inline]

instance Std.Time.Internal.Bounded.instDecidableLe {rel : Int → Int → Prop} {a b : Int} {x y : Bounded rel a b} : Decidable (x ≤ y)

Equations

• Std.Time.Internal.Bounded.instDecidableLe = inferInstanceAs (Decidable (x.val ≤ y.val))

@[reducible, inline]

abbrev Std.Time.Internal.Bounded.LE (lo hi : Int) : Type

A Bounded integer that the relation used is the the less-equal relation so, it includes all integers that lo ≤ val ≤ hi.

Equations

• Std.Time.Internal.Bounded.LE = Std.Time.Internal.Bounded LE.le

Instances For

• Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast
• Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast

@[inline]

def Std.Time.Internal.Bounded.cast {rel : Int → Int → Prop} {lo₁ lo₂ hi₁ hi₂ : Int} (h₁ : lo₁ = lo₂) (h₂ : hi₁ = hi₂) (b : Bounded rel lo₁ hi₁) : Bounded rel lo₂ hi₂

Casts the boundaries of the Bounded using equivalences.

Equations

• Std.Time.Internal.Bounded.cast h₁ h₂ b = ⟨b.val, ⋯⟩

@[reducible, inline]

abbrev Std.Time.Internal.Bounded.LT (lo hi : Int) : Type

A Bounded integer that the relation used is the the less-than relation so, it includes all integers that lo < val < hi.

Equations

• Std.Time.Internal.Bounded.LT = Std.Time.Internal.Bounded LT.lt

@[inline]

def Std.Time.Internal.Bounded.mk {lo hi : Int} {rel : Int → Int → Prop} (val : Int) (proof : rel lo val ∧ rel val hi) : Bounded rel lo hi

Creates a new Bounded Integer.

Equations

• Std.Time.Internal.Bounded.mk val proof = ⟨val, proof⟩

@[inline]

def Std.Time.Internal.Bounded.ofInt? {rel : Int → Int → Prop} {lo hi : Int} [DecidableRel rel] (val : Int) : Option (Bounded rel lo hi)

Convert a Int to a Bounded if it checks.

Equations

• Std.Time.Internal.Bounded.ofInt? val = if h : rel lo val ∧ rel val hi then some ⟨val, h⟩ else none

@[inline]

def Std.Time.Internal.Bounded.LE.ofNatWrapping {lo hi : Int} (val : Int) (h : lo ≤ hi) : LE lo hi

Convert a Nat to a Bounded.LE by wrapping it.

Equations

• Std.Time.Internal.Bounded.LE.ofNatWrapping val h = ⟨((val - lo) % (hi - lo + 1) + (hi - lo + 1)) % (hi - lo + 1) + lo, ⋯⟩

instance Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast {lo : Int} {n k : Nat} : OfNat (LE lo (lo + ↑k)) n

Equations

• Std.Time.Internal.Bounded.LE.instOfNatHAddIntCast = { ofNat := let h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping (↑n) h }

instance Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast {lo : Int} {k : Nat} : Inhabited (LE lo (lo + ↑k))

Equations

• Std.Time.Internal.Bounded.LE.instInhabitedHAddIntCast = { default := let h := ⋯; Std.Time.Internal.Bounded.LE.ofNatWrapping lo h }

@[inline]

def Std.Time.Internal.Bounded.LE.mk {lo hi : Int} (val : Int) (proof : lo ≤ val ∧ val ≤ hi) : LE lo hi

Creates a new Bounded integer that the relation is less-equal.

Equations

• Std.Time.Internal.Bounded.LE.mk val proof = ⟨val, proof⟩

@[inline]

def Std.Time.Internal.Bounded.LE.exact (val : Nat) : LE ↑val ↑val

Creates a new Bounded integer that the relation is less-equal.

Equations

• Std.Time.Internal.Bounded.LE.exact val = ⟨↑val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.ofInt {lo hi : Int} (val : Int) : Option (LE lo hi)

Creates a new Bounded integer.

Equations

• Std.Time.Internal.Bounded.LE.ofInt val = if h : lo ≤ val ∧ val ≤ hi then some ⟨val, h⟩ else none

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat {hi : Nat} (val : Nat) (h : val ≤ hi) : LE 0 ↑hi

Convert a Nat to a Bounded.LE.

Equations

• Std.Time.Internal.Bounded.LE.ofNat val h = Std.Time.Internal.Bounded.mk ↑val ⋯

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat? {hi : Nat} (val : Nat) : Option (LE 0 ↑hi)

Convert a Nat to a Bounded.LE if it checks.

Equations

• Std.Time.Internal.Bounded.LE.ofNat? val = if h : val ≤ hi then some (Std.Time.Internal.Bounded.LE.ofNat val h) else none

@[inline]

def Std.Time.Internal.Bounded.LE.ofNat' {lo hi : Nat} (val : Nat) (h : lo ≤ val ∧ val ≤ hi) : LE ↑lo ↑hi

Convert a Nat to a Bounded.LE using the lower boundary too.

Equations

• Std.Time.Internal.Bounded.LE.ofNat' val h = Std.Time.Internal.Bounded.mk ↑val ⋯

@[inline]

def Std.Time.Internal.Bounded.LE.clip {lo hi : Int} (val : Int) (h : lo ≤ hi) : LE lo hi

Convert a Nat to a Bounded.LE using the lower boundary too.

Equations

• Std.Time.Internal.Bounded.LE.clip val h = if h₀ : lo ≤ val then if h₁ : val ≤ hi then ⟨val, ⋯⟩ else ⟨hi, ⋯⟩ else ⟨lo, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.toNat {lo hi : Int} (n : LE lo hi) : Nat

Convert a Bounded.LE to a Nat.

Equations

• n.toNat = n.val.toNat

@[inline]

def Std.Time.Internal.Bounded.LE.toNat' {lo hi : Int} (n : LE lo hi) (h : lo ≥ 0) : Nat

Convert a Bounded.LE to a Nat.

Equations

• n.toNat' h = match n.val, ⋯ with | Int.ofNat n, x => n | Int.negSucc a, h => ⋯.elim

@[inline]

def Std.Time.Internal.Bounded.LE.toInt {lo hi : Int} (n : LE lo hi) : Int

Convert a Bounded.LE to an Int.

Equations

• n.toInt = n.val

@[inline]

def Std.Time.Internal.Bounded.LE.toFin {lo hi : Int} (n : LE lo hi) (h₀ : 0 ≤ lo) : Fin (hi + 1).toNat

Convert a Bounded.LE to a Fin.

Equations

• n.toFin h₀ = ⟨n.val.toNat, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.ofFin {hi : Nat} (fin : Fin hi.succ) : LE 0 ↑hi

Convert a Fin to a Bounded.LE.

Equations

• Std.Time.Internal.Bounded.LE.ofFin fin = Std.Time.Internal.Bounded.LE.ofNat ↑fin ⋯

@[inline]

def Std.Time.Internal.Bounded.LE.ofFin' {hi lo : Nat} (fin : Fin hi.succ) (h : lo ≤ hi) : LE ↑lo ↑hi

Convert a Fin to a Bounded.LE.

Equations

• Std.Time.Internal.Bounded.LE.ofFin' fin h = if h₁ : ↑fin ≥ lo then Std.Time.Internal.Bounded.LE.ofNat' ↑fin ⋯ else Std.Time.Internal.Bounded.LE.ofNat' lo ⋯

@[inline]

def Std.Time.Internal.Bounded.LE.byEmod (b i : Int) (hi : i > 0) : LE 0 (i - 1)

Creates a new Bounded.LE using a the modulus of a number.

Equations

• Std.Time.Internal.Bounded.LE.byEmod b i hi = ⟨b % i, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.byMod (b i : Int) (hi : 0 < i) : LE (-(i - 1)) (i - 1)

Creates a new Bounded.LE using a the Truncating modulus of a number.

Equations

• Std.Time.Internal.Bounded.LE.byMod b i hi = ⟨b.tmod i, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.truncate {n m : Int} (bounded : LE n m) : LE 0 (m - n)

Adjust the bounds of a Bounded by setting the lower bound to zero and the maximum value to (m - n).

Equations

• bounded.truncate = match ⋯ with | ⋯ => ⟨bounded.val - n, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.truncateTop {n m j : Int} (bounded : LE n m) (h : bounded.val ≤ j) : LE n j

Adjust the bounds of a Bounded by changing the higher bound if another value j satisfies the same constraint.

Equations

• bounded.truncateTop h = ⟨bounded.val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.truncateBottom {n m j : Int} (bounded : LE n m) (h : bounded.val ≥ j) : LE j m

Adjust the bounds of a Bounded by changing the lower bound if another value j satisfies the same constraint.

Equations

• bounded.truncateBottom h = ⟨bounded.val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.neg {n m : Int} (bounded : LE n m) : LE (-m) (-n)

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

Equations

• bounded.neg = ⟨-bounded.val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.add {n m : Int} (bounded : LE n m) (num : Int) : LE (n + num) (m + num)

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

Equations

• bounded.add num = ⟨bounded.val + num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.addProven {n m num : Int} (bounded : LE n m) (h₀ : bounded.val + num ≤ m) (h₁ : num ≥ 0) : LE n m

Adjust the bounds of a Bounded by adding a constant value to both the lower and upper bounds.

Equations

• bounded.addProven h₀ h₁ = ⟨bounded.val + num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.addTop {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE n (m + num)

Adjust the bounds of a Bounded by adding a constant value to the upper bounds.

Equations

• bounded.addTop num h = ⟨bounded.val + num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.subBottom {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE (n - num) m

Adjust the bounds of a Bounded by adding a constant value to the lower bounds.

Equations

• bounded.subBottom num h = ⟨bounded.val - num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.addBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) : LE (n + i) (m + j)

Adds two Bounded and adjust the boundaries.

Equations

• bounded.addBounds bounded₂ = ⟨bounded.val + bounded₂.val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.sub {n m : Int} (bounded : LE n m) (num : Int) : LE (n - num) (m - num)

Adjust the bounds of a Bounded by subtracting a constant value to both the lower and upper bounds.

Equations

• bounded.sub num = bounded.add (-num)

@[inline]

def Std.Time.Internal.Bounded.LE.subBounds {n m i j : Int} (bounded : LE n m) (bounded₂ : LE i j) : LE (n - j) (m - i)

Adds two Bounded and adjust the boundaries.

Equations

• bounded.subBounds bounded₂ = bounded.addBounds bounded₂.neg

@[inline]

def Std.Time.Internal.Bounded.LE.emod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) : LE 0 (num✝ - 1)

Adjust the bounds of a Bounded by applying the emod operation constraining the lower bound to 0 and the upper bound to the value.

Equations

• bounded.emod num hi = Std.Time.Internal.Bounded.LE.byEmod bounded.val num hi

@[inline]

def Std.Time.Internal.Bounded.LE.mod {n num : Int} (bounded : LE n num) (num✝ : Int) (hi : 0 < num✝) : LE (-(num✝ - 1)) (num✝ - 1)

Adjust the bounds of a Bounded by applying the mod operation.

Equations

• bounded.mod num hi = Std.Time.Internal.Bounded.LE.byMod bounded.val num hi

@[inline]

def Std.Time.Internal.Bounded.LE.mul_pos {n m : Int} (bounded : LE n m) (num : Int) (h : num ≥ 0) : LE (n * num) (m * num)

Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

Equations

• bounded.mul_pos num h = ⟨bounded.val * num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.mul_neg {n m : Int} (bounded : LE n m) (num : Int) (h : num ≤ 0) : LE (m * num) (n * num)

Adjust the bounds of a Bounded by applying the multiplication operation with a positive number.

Equations

• bounded.mul_neg num h = ⟨bounded.val * num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.ediv {n m : Int} (bounded : LE n m) (num : Int) (h : num > 0) : LE (n / num) (m / num)

Adjust the bounds of a Bounded by applying the div operation.

Equations

• bounded.ediv num h = match ⋯ with | ⋯ => ⟨bounded.val.ediv num, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.eq {n : Int} : LE n n

Equations

• Std.Time.Internal.Bounded.LE.eq = ⟨n, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.expand {lo hi nhi nlo : Int} (bounded : LE lo hi) (h : hi ≤ nhi) (h₁ : nlo ≤ lo) : LE nlo nhi

Expand the range of a bounded value.

Equations

• bounded.expand h h₁ = ⟨bounded.val, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.expandTop {lo hi nhi : Int} (bounded : LE lo hi) (h : hi ≤ nhi) : LE lo nhi

Expand the bottom of the bounded to a number nhi is hi is less or equal to the previous higher bound.

Equations

• bounded.expandTop h = bounded.expand h ⋯

@[inline]

def Std.Time.Internal.Bounded.LE.expandBottom {lo hi nlo : Int} (bounded : LE lo hi) (h : nlo ≤ lo) : LE nlo hi

Expand the bottom of the bounded to a number nlo if lo is greater or equal to the previous lower bound.

Equations

• bounded.expandBottom h = bounded.expand ⋯ h

@[inline]

def Std.Time.Internal.Bounded.LE.succ {lo hi : Int} (bounded : LE lo hi) (h : bounded.val < hi) : LE lo hi

Adds one to the value of the bounded if the value is less than the higher bound of the bounded number.

Equations

• bounded.succ h = ⟨bounded.val + 1, ⋯⟩

@[inline]

def Std.Time.Internal.Bounded.LE.abs {i : Int} (bo : LE (-i) i) : LE 0 i

Returns the absolute value of the bounded number bo with bounds -(i - 1) to i - 1. The result will be a new bounded number with bounds 0 to i - 1.

Equations

• bo.abs = if h : bo.val ≥ 0 then bo.truncateBottom h else let r := (bo.truncateTop ⋯).neg; ⋯.mp r

def Std.Time.Internal.Bounded.LE.max {n m : Int} (bounded : LE n m) (val : Int) : LE (Max.max n val) (Max.max m val)

Returns the maximum between a number and the bounded.

Equations

• bounded.max val = match ⋯ with | ⋯ => ⟨max bounded.val val, ⋯⟩