Module mathcomp.analysis.itv

# Numbers within an intervel This file develops tools to make the manipulation of numbers within a known interval easier, thanks to canonical structures. This adds types like {itv R & `[a, b]}, a notation e%:itv that infers an enclosing interval for expression e according to existing canonical instances and %:inum to cast back from type {itv R & i} to R. For instance, x : {i01 R}, we have (1 - x%:inum)%:itv : {i01 R} automatically inferred. ## types for values within known interval ``` {i01 R} == interface type for elements in R that live in `[0, 1]; R must have a numDomainType structure. Allows to solve automatically goals of the form x >= 0 and x <= 1 if x is canonically a {i01 R}. {i01 R} is canonically stable by common operations. {itv R & i} == more generic type of values in interval i : interval int R must have a numDomainType structure. This type is shown to be a porderType. ``` ## casts from/to values within known interval ``` x%:itv == explicitly casts x to the most precise known {itv R & i} according to existing canonical instances. x%:i01 == explicitly casts x to {i01 R} according to existing canonical instances. x%:inum == explicit cast from {itv R & i} to R. ``` ## sign proofs ``` [itv of x] == proof that x is in interval inferred by x%:itv [lb of x] == proof that lb < x or lb <= x with lb the lower bound inferred by x%:itv [ub of x] == proof that x < ub or x <= ub with ub the upper bound inferred by x%:itv [lbe of x] == proof that lb <= x [ube of x] == proof that x <= ub ``` ## constructors ``` ItvNum xin == builds a {itv R & i} from a proof xin : x \in i where x : R ``` A number of canonical instances are provided for common operations, if your favorite operator is missing, look below for examples on how to add the appropriate Canonical. Canonical instances are also provided according to types, as a fallback when no known operator appears in the expression. Look to itv_top_typ below for an example on how to add your favorite type.