Statistics

─── Uninterpreted refinement-language symbols ───────────────────────── These live in the refinement language so Z3 can reason about them as abstract symbols. Runtime providers below tie concrete values back to them via refined return types. Fraction of xs strictly below threshold t.
Imports
open Array;
Table of Contents

Functions

widenBelow

Monotonicity below: t1 <= t2 ⇒ fracBelow xs t1 <= fracBelow xs t2.
def widenBelow (xs: {x : Array Float | Array.size x > 0}) (t1: Float) (t2: {t : Float | t ≥ t1}) : {r : Array Float | Array.size r > 0 && fracBelow r t2 ≥ fracBelow xs t1}

widenAbove

Monotonicity above: t1 <= t2 ⇒ fracAbove xs t1 >= fracAbove xs t2.
def widenAbove (xs: {x : Array Float | Array.size x > 0}) (t1: Float) (t2: {t : Float | t ≤ t1}) : {r : Array Float | Array.size r > 0 && fracAbove r t2 ≥ fracAbove xs t1}

belowComplement

Complement at a non-atomic point: fracBelow + fracAbove = 1.
def belowComplement (xs: {x : Array Float | Array.size x > 0}) (t: Float) : {r : Array Float | Array.size r > 0 && fracBelow r t = 1.0 - fracAbove xs t}

betweenFromBelow

Between bound: fracBetween lo hi >= fracBelow hi - fracBelow lo (slack covers atoms).
def betweenFromBelow (xs: {x : Array Float | Array.size x > 0}) (lo: Float) (hi: {h : Float | h ≥ lo}) : {r : Array Float | Array.size r > 0 && fracBetween r lo hi ≥ fracBelow xs hi - fracBelow xs lo}

mean

Returns the mean (average) of a non-empty list of numbers.
def mean (xs: {x : Array Float | Array.size x > 0}) : {m : Float | m = sampleMean xs}

median

Returns the median (middle value) of a non-empty list of numbers.
def median (xs: {x : Array Float | Array.size x > 0}) : Float

std

Returns the sample standard deviation of a non-empty list of numbers.
def std (xs: {x : Array Float | Array.size x > 0}) : {s : Float | s = sampleStd xs}

var

Returns the sample variance of a non-empty list of numbers.
def var (xs: {x : Array Float | Array.size x > 0}) : {v : Float | v = sampleVar xs}

min

Returns the minimum value in a non-empty list of numbers.
def min (xs: {x : Array Float | Array.size x > 0}) : {m : Float | m = sampleMin xs}

max

Returns the maximum value in a non-empty list of numbers.
def max (xs: {x : Array Float | Array.size x > 0}) : {m : Float | m = sampleMax xs}

sum

Returns the sum of a non-empty list of numbers.
def sum (xs: {x : Array Float | Array.size x > 0}) : Float

quantile

Returns the quantile of a non-empty list of numbers.
def quantile (xs: {x : Array Float | Array.size x > 0}) (q: Float) : Float

prod

Returns the product of a non-empty list of numbers.
def prod (xs: {x : Array Float | Array.size x > 0}) : Float

cumsum

Returns the cumulative sum of a non-empty list of numbers.
def cumsum (xs: {x : Array Float | Array.size x > 0}) : Array Float

cumprod

Returns the cumulative product of a non-empty list of numbers.
def cumprod (xs: {x : Array Float | Array.size x > 0}) : Array Float

quartiles

Returns the 1st (Q1), 2nd (median), and 3rd (Q3) quartiles of a non-empty list of numbers.
def quartiles (xs: {x : Array Float | Array.size x > 0}) : Array Float

unique

Returns the unique values in a non-empty list.
def unique (xs: {x : Array Float | Array.size x > 0}) : Array Float

argmax

Returns the index of the maximum value in a non-empty list of numbers.
def argmax (xs: {x : Array Float | Array.size x > 0}) : Float

argmin

Returns the index of the minimum value in a non-empty list of numbers.
def argmin (xs: {x : Array Float | Array.size x > 0}) : Float

percentile

Returns the percentile of a non-empty list of numbers.
def percentile (xs: {x : Array Float | Array.size x > 0}) (p: Float) : Float

corrcoef

Returns the correlation coefficient of two non-empty lists of equal length.
def corrcoef (xs: {x : Array Float | Array.size x > 0}) (ys: {y : Array Float | Array.size y = Array.size xs}) : Float

cov

Returns the covariance of two non-empty lists of equal length.
def cov (xs: {x : Array Float | Array.size x > 0}) (ys: {y : Array Float | Array.size y = Array.size xs}) : Float

proportionBelow

Proportion of values strictly below a threshold.
def proportionBelow (xs: {x : Array Float | Array.size x > 0}) (t: Float) : {f : Float | f = fracBelow xs t && (0.0 ≤ f && f ≤ 1.0)}

proportionAbove

Proportion of values strictly above a threshold.
def proportionAbove (xs: {x : Array Float | Array.size x > 0}) (t: Float) : {f : Float | f = fracAbove xs t && (0.0 ≤ f && f ≤ 1.0)}

proportionBetween

Proportion of values strictly inside the open interval (lo, hi).
def proportionBetween (xs: {x : Array Float | Array.size x > 0}) (lo: Float) (hi: {h : Float | h ≥ lo}) : {f : Float | f = fracBetween xs lo hi && (0.0 ≤ f && f ≤ 1.0)}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

fracBelow

uninterpreted
Fraction of xs strictly below threshold t.
def fracBelow : (xs : Array Float) → (t : Float) → Float

fracAbove

uninterpreted
Fraction of xs strictly above threshold t.
def fracAbove : (xs : Array Float) → (t : Float) → Float

fracBetween

uninterpreted
Fraction of xs in the open interval (lo, hi).
def fracBetween : (xs : Array Float) → (lo : Float) → (hi : Float) → Float

sampleMean

uninterpreted
Sample summary statistics as abstract symbols.
def sampleMean : (xs : Array Float) → Float

sampleVar

uninterpreted
def sampleVar : (xs : Array Float) → Float

sampleStd

uninterpreted
def sampleStd : (xs : Array Float) → Float

sampleMin

uninterpreted
def sampleMin : (xs : Array Float) → Float

sampleMax

uninterpreted
def sampleMax : (xs : Array Float) → Float