This file develops tools to make the manipulation of numbers with a known sign easier, thanks to canonical structures. This adds types like {posnum R} for positive values in R, a notation e%:pos that infers the positivity of expression e according to existing canonical instances and %:num to cast back from type {posnum R} to R. For instance, given x, y : {posnum R}, we have ((x%:num + y%:num) / 2)%:pos : {posnum R} automatically inferred.

types for values with known sign

{posnum R} == interface type for elements in R that are positive; R must have a zmodType structure. Allows to solve automatically goals of the form x > 0 if x is canonically a {posnum R}. {posnum R} is canonically stable by common operations. All positive natural numbers ((n.+1)%:R) are also canonically in {posnum R} {nonneg R} == interface types for elements in R that are non-negative; R must have a zmodType structure. Automatically solves goals of the form x >= 0. {nonneg R} is stable by common operations. All natural numbers n%:R are also canonically in {nonneg R}. {compare x0 & nz & cond} == more generic type of values comparing to x0 : T according to nz and cond (see below). T must have a porderType structure. This type is shown to be a porderType. It is also an orderTpe, as soon as T is a numDomainType. {num R & nz & cond} == {compare 0%R : R & nz & cond}. T must have a zmodType structure. {= x0} == {compare x0 & ?=0 & =0} {= x0 : T} == same with an explicit type T {> x0} == {compare x0 & !=0 & >=0} {> x0 : T} == same with an explicit type T {< x0} == {compare x0 & !=0 & <=0} {< x0 : T} == same with an explicit type T {>= x0} == {compare x0 & ?=0 & >=0} {>= x0 : T} == same with an explicit type T {<= x0} == {compare x0 & ?=0 & <=0} {<= x0 : T} == same with an explicit type T {>=< x0} == {compare x0 & ?=0 & >=<0} {>=< x0 : T} == same with an explicit type T {>< x0} == {compare x0 & !=0 & >=<0} {>< x0 : T} == same with an explicit type T {!= x0} == {compare x0 & !=0 & >?<0} {!= x0 : T} == same with an explicit type T {?= x0} == {compare x0 & ?=0 & >?<0} {?= x0 : T} == same with an explicit type T

casts from/to values with known sign

x%:pos == explicitly casts x to {posnum R}, triggers the inference of a {posnum R} structure for x. x%:nng == explicitly casts x to {nonneg R}, triggers the inference of a {nonneg R} structure for x. x%:sgn == explicitly casts x to the most precise known {compare x0 & nz & cond} according to existing canonical instances. x%:num == explicit cast from {compare x0 & nz & cond} to R. In particular this works from {posnum R} and {nonneg R} to R. x%:posnum == explicit cast from {posnum R} to R. x%:nngnum == explicit cast from {nonneg R} to R.

nullity conditions nz

All nz above can be the following (in scope snum_nullity_scope delimited by %snum_nullity) !=0 == to encode x != 0 ?=0 == unknown nullity

reality conditions cond

All cond above can be the following (in scope snum_sign_scope delimited by by %snum_sign) =0 == to encode x == 0 >=0 == to encode x >= 0 <=0 == to encode x <= 0 >=<0 == to encode x >=< 0 >?<0 == unknown reality

sign proofs

[sgn of x] == proof that x is of sign inferred by x%:sgn [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

PosNum xgt0 == builds a {posnum R} from a proof xgt0 : x > 0 where x : R NngNum xge0 == builds a {posnum R} from a proof xgt0 : x >= 0 where x : R Signed.mk p == builds a {compare x0 & nz & cond} from a proof p that some x satisfies sign conditions encoded by nz and cond

misc

!! x == triggers pretyping to fill the holes of the term x. The main use case is to trigger typeclass inference in the body of a ssreflect have := !! body. Credits: Enrico Tassi. 2 == notation for 2%: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 nat_snum below for an example on how to add your favorite type.

infer class to help typeclass inference on the fly

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

Section Order. Variables (d : unit) (T : orderType d) (x0 : T) (nz : nullity) (cond : reality). Local Notation sT := {compare x0 & nz & cond}. Lemma signed_le_total : totalPOrderMixin [porderType of sT]. Proof. by move=> x y; apply: le_total. Qed. Canonical signed_latticeType := LatticeType sT signed_le_total. Canonical signed_distrLatticeType := DistrLatticeType sT signed_le_total. Canonical signed_orderType := OrderType sT signed_le_total. End Order.