Documentation

Time.Fixed

structure Time.Fixed (precision : Nat) :

fixed-point representation of a fractional number

val : Int

Instances For

theorem Time.Fixed.ext {precision : Nat} {x y : Fixed precision} (val : x.val = y.val) :

x = y

instance Time.instReprFixed {precision✝ : Nat} :

Repr (Fixed precision✝)

Equations

Time.instReprFixed = { reprPrec := Time.reprFixed✝ }

instance Time.instBEqFixed {precision✝ : Nat} :

BEq (Fixed precision✝)

Equations

Time.instBEqFixed = { beq := Time.beqFixed✝ }

instance Time.instDecidableEqFixed {precision✝ : Nat} :

DecidableEq (Fixed precision✝)

Equations

Time.instDecidableEqFixed = Time.decEqFixed✝

inductive Time.Sign :

Nonneg : Sign
Neg : Sign

Instances For

instance Time.instReprSign :

Equations

Time.instReprSign = { reprPrec := Time.reprSign✝ }

instance Time.instBEqSign :

Equations

Time.instBEqSign = { beq := Time.beqSign✝ }

instance Time.instDecidableEqSign :

DecidableEq Sign

Equations

Time.instDecidableEqSign x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure Time.Fixed.Denominator (precision : Nat) :

denominator of Fixed p

val : Nat
lt : self.val < 10 ^ precision

Instances For

instance Time.Fixed.instReprDenominator {precision✝ : Nat} :

Repr (Denominator precision✝)

Equations

Time.Fixed.instReprDenominator = { reprPrec := Time.Fixed.reprDenominator✝ }

instance Time.Fixed.instBEqDenominator {precision✝ : Nat} :

BEq (Denominator precision✝)

Equations

Time.Fixed.instBEqDenominator = { beq := Time.Fixed.beqDenominator✝ }

instance Time.Fixed.instDecidableEqDenominator {precision✝ : Nat} :

DecidableEq (Denominator precision✝)

Equations

Time.Fixed.instDecidableEqDenominator = Time.Fixed.decEqDenominator✝

structure Time.Fixed.Parts (precision : Nat) :

parts of Fixed p

sign : Sign
numerator : Nat
denominator : Nat
lt : self.denominator < 10 ^ precision

Instances For

instance Time.Fixed.instReprParts {precision✝ : Nat} :

Repr (Parts precision✝)

Equations

Time.Fixed.instReprParts = { reprPrec := Time.Fixed.reprParts✝ }

instance Time.Fixed.instBEqParts {precision✝ : Nat} :

BEq (Parts precision✝)

Equations

Time.Fixed.instBEqParts = { beq := Time.Fixed.beqParts✝ }

instance Time.Fixed.instDecidableEqParts {precision✝ : Nat} :

DecidableEq (Parts precision✝)

Equations

Time.Fixed.instDecidableEqParts = Time.Fixed.decEqParts✝

def Time.Fixed.zero {p : Nat} :

Equations

Time.Fixed.zero = { val := 0 }

Instances For

def Time.Fixed.Denominator.zero {p : Nat} :

Equations

Time.Fixed.Denominator.zero = { val := 0, lt := ⋯ }

Instances For

instance Time.instInhabitedFixed {p : Nat} :

Inhabited (Fixed p)

Equations

Time.instInhabitedFixed = { default := Time.Fixed.zero }

instance Time.instLTFixed {p : Nat} :

Equations

Time.instLTFixed = { lt := fun (a b : Time.Fixed p) => a.val < b.val }

theorem Time.lt_def {p : Nat} (a b : Fixed p) :

(a < b) = (a.val < b.val)

instance Time.instLEFixed {p : Nat} :

Equations

Time.instLEFixed = { le := fun (a b : Time.Fixed p) => a.val ≤ b.val }

instance Time.instLeReflFixed {p : Nat} :

LeRefl (Fixed p)

theorem Time.le_def {p : Nat} (a b : Fixed p) :

(a ≤ b) = (a.val ≤ b.val)

instance Time.instInhabitedDenominator {p : Nat} :

Inhabited (Fixed.Denominator p)

Equations

Time.instInhabitedDenominator = { default := Time.Fixed.Denominator.zero }

theorem Time.inhabited_def {p : Nat} :

default = Fixed.Denominator.zero

instance Time.instLTDenominator {p : Nat} :

LT (Fixed.Denominator p)

Equations

Time.instLTDenominator = { lt := fun (a b : Time.Fixed.Denominator p) => a.val < b.val }

instance Time.instLEDenominator {p : Nat} :

LE (Fixed.Denominator p)

Equations

Time.instLEDenominator = { le := fun (a b : Time.Fixed.Denominator p) => a.val ≤ b.val }

instance Time.instLeReflDenominator {p : Nat} :

LeRefl (Fixed.Denominator p)

def Time.Fixed.neg {p : Nat} (f : Fixed p) :

Equations

f.neg = { val := -f.val }

Instances For

def Time.Fixed.toParts {p : Nat} (f : Fixed p) :

Equations

f.toParts = { sign := if f.val < 0 then Time.Sign.Neg else Time.Sign.Nonneg, numerator := f.val.natAbs / 10 ^ p, denominator := f.val.natAbs % 10 ^ p, lt := ⋯ }

Instances For

def Time.Fixed.toFixed {p : Nat} (sign : Sign) (num : Nat) (denom : Denominator p) :

Equations

Time.Fixed.toFixed Time.Sign.Neg num denom = { val := Int.negOfNat (num * 10 ^ p + denom.val) }
Time.Fixed.toFixed Time.Sign.Nonneg num denom = { val := ↑num * 10 ^ p + ↑denom.val }

Instances For

def Time.Fixed.Parts.fromParts {p : Nat} (parts : Parts p) :

Equations

parts.fromParts = Time.Fixed.toFixed parts.sign parts.numerator { val := parts.denominator, lt := ⋯ }

Instances For

def Time.Fixed.toSign (n : Int) :

Equations

Time.Fixed.toSign n = if n < 0 then Time.Sign.Neg else Time.Sign.Nonneg

Instances For

def Time.Fixed.toDenominator (n p : Nat) (h : n < 10 ^ p) :

Equations

Time.Fixed.toDenominator n p h = { val := n, lt := h }

Instances For

def Time.Fixed.denominatorValueToString (d : Int) (p : Nat) :

Equations

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

Instances For

def Time.Fixed.denominatorToString {p : Nat} (f : Fixed p) :

Equations

f.denominatorToString = match f.toParts with | { sign := sign, numerator := numerator, denominator := d, lt := lt } => Time.Fixed.denominatorValueToString (↑d) p

Instances For

instance Time.Fixed.instToString {p : Nat} :

ToString (Fixed p)

Equations

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

def Time.Fixed.sub {p : Nat} (dt1 dt2 : Fixed p) :

Equations

dt1.sub dt2 = { val := dt1.val - dt2.val }

Instances For

def Time.Fixed.add {p : Nat} (dt1 dt2 : Fixed p) :

Equations

dt1.add dt2 = { val := dt1.val + dt2.val }

Instances For

instance Time.Fixed.instSub {p : Nat} :

Equations

Time.Fixed.instSub = { sub := Time.Fixed.sub }

theorem Time.Fixed.sub_def {p : Nat} (a b : Fixed p) :

a - b = a.sub b

instance Time.Fixed.instAdd {p : Nat} :

Equations

Time.Fixed.instAdd = { add := Time.Fixed.add }

theorem Time.Fixed.add_def {p : Nat} (a b : Fixed p) :

a + b = a.add b

def Time.Fixed.Int.toFixed (n : Int) (p : Nat) :

Equations

Time.Fixed.Int.toFixed n p = { val := n }

Instances For

def Time.Fixed.div {p : Nat} (dt1 dt2 : Fixed p) :

Equations

dt1.div dt2 = dt1.val / dt2.val

Instances For

instance Time.Fixed.instHDivInt {p : Nat} :

HDiv (Fixed p) (Fixed p) Int

Equations

Time.Fixed.instHDivInt = { hDiv := Time.Fixed.div }

theorem Time.Fixed.div_def {p : Nat} (a b : Fixed p) :

a / b = a.div b

def Time.Fixed.mul {p : Nat} (a : Int) (f : Fixed p) :

Equations

Time.Fixed.mul a f = { val := a * f.val }

Instances For

instance Time.Fixed.instHMulInt {p : Nat} :

HMul Int (Fixed p) (Fixed p)

Equations

Time.Fixed.instHMulInt = { hMul := Time.Fixed.mul }

theorem Time.Fixed.mul_def {p : Nat} (a : Int) (b : Fixed p) :

a * b = mul a b

def Time.Fixed.mod {p : Nat} (dt1 dt2 : Fixed p) :

Equations

dt1.mod dt2 = { val := dt1.val % dt2.val }

Instances For

instance Time.Fixed.instMod {p : Nat} :

Equations

Time.Fixed.instMod = { mod := Time.Fixed.mod }

theorem Time.Fixed.mod_def {p : Nat} (a b : Fixed p) :

a % b = a.mod b

@[simp]

theorem Time.Fixed.ofFixed_lt {p : Nat} {a b : Fixed p} :

a < b ↔ a.val < b.val

@[simp]

theorem Time.Fixed.ofFixed_ne {p : Nat} {a b : Fixed p} :

a ≠ b ↔ a.val ≠ b.val

theorem Time.Fixed.ne_of_lt {p : Nat} {a b : Fixed p} (h : a < b) :

a ≠ b

theorem Time.Fixed.emod_nonneg {p : Nat} (a : Fixed p) {b : Fixed p} (h : b ≠ { val := 0 }) :

{ val := 0 } ≤ a % b

theorem Time.Fixed.emod_lt_of_pos {p : Nat} (a : Fixed p) {b : Fixed p} (h : { val := 0 } < b) :

a % b < b

theorem Time.Fixed.emod_add_ediv {p : Nat} (a b : Fixed p) :

a % b + a / b * b = a

def Time.Fixed.toMod {p : Nat} (n d : Fixed p) (h : zero < d) :

{ m : Fixed p // zero ≤ m ∧ m < d }

toMod computes n % d : { m : Fixed p // zero ≤ m ∧ m < d }

Equations

n.toMod d h = ⟨n % d, ⋯⟩

Instances For

theorem Time.Fixed.toFixed_lt_toFixed (p n : Nat) (n_denom : Denominator p) (m : Nat) (m_denom : Denominator p) (hnm : n < m) :

toFixed Sign.Nonneg n n_denom < toFixed Sign.Nonneg m m_denom

theorem Time.Fixed.zero_lt_toFixed (p m : Nat) (m_denom : Denominator p) (h : 0 < m) :

zero < toFixed Sign.Nonneg m m_denom

theorem Time.Fixed.toFixed_le_toFixed_of_lt (p n : Nat) (n_denom : Denominator p) (m : Nat) (m_denom : Denominator p) (hnm : n < m) :

toFixed Sign.Nonneg n n_denom ≤ toFixed Sign.Nonneg m m_denom

theorem Time.Fixed.zero_le_toFixed (p m : Nat) (m_denom : Denominator p) (hnm : 0 < m) :

zero ≤ toFixed Sign.Nonneg m m_denom

theorem Time.Fixed.fixed_eq_toParts_fromParts {p : Nat} (f : Fixed p) :

f = f.toParts.fromParts