Library mathcomp.algebra.interval_inference

md # Numbers within an interval 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 %:num to cast back from type {itv R & i} to R. For instance, for x : {i01 R}, we have (1 - x%:num)%:itv : {i01 R} automatically inferred. ## types for values within known interval ``` {itv R & i} == generic type of values in interval i : interval int See interval.v for notations that can be used for i. R must have a numDomainType structure. This type is shown to be a porderType. {i01 R} := {itv R & `[0, 1]} Allows to solve automatically goals of the form x >= 0 and x <= 1 when x is canonically a {i01 R}. {i01 R} is canonically stable by common operations. {posnum R} := {itv R & `]0, +oo[) {nonneg R} := {itv R & `[0, +oo[) ``` ## casts from/to values within known interval Explicit casts of x to some {itv R & i} according to existing canonical instances: ``` x%:itv == cast to the most precisely known {itv R & i} x%:i01 == cast to {i01 R}, or fail x%:pos == cast to {posnum R}, or fail x%:nng == cast to {nonneg R}, or fail ``` Explicit casts of x from some {itv R & i} to R: ``` x%:num == cast from {itv R & i} x%:posnum == cast from {posnum R} x%:nngnum == cast from {nonneg R} ``` ## sign proofs ``` [itv of x] == proof that x is in the interval inferred by x%:itv [gt0 of x] == proof that x > 0 [lt0 of x] == proof that x < 0 [ge0 of x] == proof that x >= 0 [le0 of x] == proof that x <= 0 [cmp0 of x] == proof that 0 >=< x [neq0 of x] == proof that x != 0 ``` ## constructors ``` ItvNum xr lx xu == builds a {itv R & i} from proofs xr : x \in Num.real, lx : map_itv_bound (Itv.num_sem R) l <= BLeft x xu : BRight x <= map_itv_bound (Itv.num_sem R) u where x : R with R : numDomainType and l u : itv_bound int ItvReal lx xu == builds a {itv R & i} from proofs lx : map_itv_bound (Itv.num_sem R) l <= BLeft x xu : BRight x <= map_itv_bound (Itv.num_sem R) u where x : R with R : realDomainType and l u : itv_bound int Itv01 x0 x1 == builds a {i01 R} from proofs x0 : 0 <= x and x1 : x <= 1 where x : R with R : numDomainType PosNum x0 == builds a {posnum R} from a proof x0 : x > 0 where x : R NngNum x0 == builds a {posnum R} from a proof x0 : x >= 0 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. Also note that all provided instances aren't necessarily optimal, improvements welcome! Canonical instances are also provided according to types, as a fallback when no known operator appears in the expression. Look to top_typ below for an example on how to add your favorite type.

First, the interval arithmetic operations we will later use

used in ereal.v

used in ereal.v

a few lifting helper functions

This adds _ <- Itv.r ( typ_inum ) to canonical projections (c.f., Print Canonical Projections Itv.r) meaning that if no other canonical instance (with a registered head symbol) is found, a canonical instance of Itv.typ, like the ones above, will be looked for.

We can't directly put an instance on Order.min for R : numDomainType since we may want instances for other porderType (typically \bar R or even nat). So we resort on this additional canonical structure.

The default instances on porderType, for min...

...and for max

Instance of the above structure for numDomainType