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.
{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
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.
All nz above can be the following (in scope snum_nullity_scope delimited
by %snum_nullity)
!=0 == to encode x != 0
?=0 == unknown nullity
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
[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
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
!! 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.
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.