Module mathcomp.reals.signed

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra.

Attributes deprecated(since="mathcomp-analysis 1.9.0",
note="Use ""From mathcomp Require Import interval_inference."" instead.").

# Positive, non-negative numbers, etc. 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. ``` 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.

Reserved Notation "{ 'compare' x0 & nz & cond }"
(format "{ 'compare' x0 & nz & cond }").
Reserved Notation "{ 'num' R & nz & cond }"
(format "{ 'num' R & nz & cond }").
Reserved Notation "{ = x0 }" (format "{ = x0 }").
Reserved Notation "{ > x0 }" (format "{ > x0 }").
Reserved Notation "{ < x0 }" (format "{ < x0 }").
Reserved Notation "{ >= x0 }" (format "{ >= x0 }").
Reserved Notation "{ <= x0 }" (format "{ <= x0 }").
Reserved Notation "{ >=< x0 }" (format "{ >=< x0 }").
Reserved Notation "{ >< x0 }" (format "{ >< x0 }").
Reserved Notation "{ != x0 }" (format "{ != x0 }").
Reserved Notation "{ ?= x0 }" (format "{ ?= x0 }").
Reserved Notation "{ = x0 : T }" (format "{ = x0 : T }").
Reserved Notation "{ > x0 : T }" (format "{ > x0 : T }").
Reserved Notation "{ < x0 : T }" (format "{ < x0 : T }").
Reserved Notation "{ >= x0 : T }" (format "{ >= x0 : T }").
Reserved Notation "{ <= x0 : T }" (format "{ <= x0 : T }").
Reserved Notation "{ >=< x0 : T }" (format "{ >=< x0 : T }").
Reserved Notation "{ >< x0 : T }" (format "{ >< x0 : T }").
Reserved Notation "{ != x0 : T }" (format "{ != x0 : T }").
Reserved Notation "{ ?= x0 : T }" (format "{ ?= x0 : T }").
Reserved Notation "=0" (format "=0").
Reserved Notation ">=0" (format ">=0").
Reserved Notation "<=0" (format "<=0").
Reserved Notation ">=<0" (format ">=<0").
Reserved Notation ">?<0" (format ">?<0").
Reserved Notation "!=0" (format "!=0").
Reserved Notation "?=0" (format "?=0").

Reserved Notation "x %:sgn" (format "x %:sgn").
Reserved Notation "x %:num" (format "x %:num").
Reserved Notation "x %:posnum" (format "x %:posnum").
Reserved Notation "x %:nngnum" (format "x %:nngnum").
Reserved Notation "[ 'sgn' 'of' x ]" (format "[ 'sgn' 'of' x ]").
Reserved Notation "[ 'gt0' 'of' x ]" (format "[ 'gt0' 'of' x ]").
Reserved Notation "[ 'lt0' 'of' x ]" (format "[ 'lt0' 'of' x ]").
Reserved Notation "[ 'ge0' 'of' x ]" (format "[ 'ge0' 'of' x ]").
Reserved Notation "[ 'le0' 'of' x ]" (format "[ 'le0' 'of' x ]").
Reserved Notation "[ 'cmp0' 'of' x ]" (format "[ 'cmp0' 'of' x ]").
Reserved Notation "[ 'neq0' 'of' x ]" (format "[ 'neq0' 'of' x ]").

Reserved Notation "{ 'posnum' R }" (format "{ 'posnum' R }").
Reserved Notation "{ 'nonneg' R }" (format "{ 'nonneg' R }").
Reserved Notation "x %:pos" (format "x %:pos").
Reserved Notation "x %:nng" (format "x %:nng").

Reserved Notation "!! x" (at level 100, only parsing).

Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory Order.Syntax.
Import GRing.Theory Num.Theory.

Local Open Scope ring_scope.
Local Open Scope order_scope.

Declare Scope snum_scope.
Delimit Scope snum_scope with snum.
Declare Scope snum_sign_scope.
Delimit Scope snum_sign_scope with snum_sign.
Declare Scope snum_nullity_scope.
Delimit Scope snum_nullity_scope with snum_nullity.

Notation := (ltac:(refine x)) (only parsing).
Class ( : Prop) := : P.
#[global] Hint Mode infer ! : typeclass_instances.
#[global] Hint Extern 0 (infer _) => (exact) : typeclass_instances.
Lemma ( : Prop) : P -> infer P

Proof.

by []. Qed.

Module Import .
Variant := | .
Coercion := if nz is NonZero then true else false.
Definition := if b then NonZero else MaybeZero.

Variant := | | .
Variant := of sign | .
Variant := of real | .

Definition :=
  match xnz, ynz with
  | MaybeZero, _
  | NonZero, NonZero => true
  | NonZero, MaybeZero => false
  end.
Definition :=
  match xs, ys with
  | NonNeg, NonNeg | NonNeg, EqZero
  | NonPos, NonPos | NonPos, EqZero
  | EqZero, EqZero => true
  | NonNeg, NonPos | NonPos, NonNeg
  | EqZero, NonPos | EqZero, NonNeg => false
  end.
Definition :=
  match xr, yr with
  | AnySign, _ => true
  | Sign sx, Sign sy => wider_sign sx sy
  | Sign _, AnySign => false
  end.
Definition :=
  match xr, yr with
  | Arbitrary, _ => true
  | Real xr, Real yr => wider_real xr yr
  | Real _, Arbitrary => false
  end.
End KnownSign.

Module .
Section Signed.
Context ( : Order.disp_t) ( : porderType disp) ( : T).

Local Coercion := if r is Real _ then true else false.
Definition ( : reality) ( : T) :=
  match n with
  | Real (Sign EqZero) => x == x0
  | Real (Sign NonNeg) => x >= x0
  | Real (Sign NonPos) => x <= x0
  | Real AnySign       => (x0 <= x) || (x <= x0)
  | Arbitrary          => true
  end.

Record ( : nullity) ( : reality) := Def {
   :> T;
  #[canonical=no]
   : (nz ==> (r != x0)) && reality_cond cond r
}.

End Signed.

Notation x0 nz cond x :=
  ((nullity_bool nz%snum_nullity ==> (x != x0))
   && (reality_cond x0 cond%snum_sign x)).

Record := Typ {
   : porderType d;
  #[canonical=no]
   : sort;
  #[canonical=no]
   : forall : sort, spec sort_x0 nz cond x
}.

Definition { } : @def d T x0 nz cond :=
  @Def d T x0 nz cond r P.

Definition { }
  { : @def d T x0 nz cond} ( : phantom T x) := x.

Definition { }
  { : @def d T x0 nz cond} ( : phantom T x) := P x.

Module .
Coercion Sign : sign >-> real.
Coercion Real : real >-> reality.
Coercion is_real : reality >-> bool.
Bind Scope snum_sign_scope with sign.
Bind Scope snum_sign_scope with reality.
Bind Scope snum_nullity_scope with nullity.
Notation := EqZero : snum_sign_scope.
Notation := NonNeg : snum_sign_scope.
Notation := NonPos : snum_sign_scope.
Notation := AnySign : snum_sign_scope.
Notation := Arbitrary : snum_sign_scope.
Notation := NonZero : snum_nullity_scope.
Notation := MaybeZero : snum_nullity_scope.
Notation := (def x0 nz cond) : type_scope.
Notation := (def (0%R : R) nz cond) : ring_scope.
Notation := (def (x0 : T) MaybeZero EqZero) : type_scope.
Notation := (def (x0 : T) NonZero NonNeg) : type_scope.
Notation := (def (x0 : T) NonZero NonPos) : type_scope.
Notation := (def (x0 : T) MaybeZero NonNeg) : type_scope.
Notation := (def (x0 : T) MaybeZero NonPos) : type_scope.
Notation := (def (x0 : T) NonZero Real) : type_scope.
Notation := (def (x0 : T) MaybeZero Real) : type_scope.
Notation := (def (x0 : T) NonZero Arbitrary) : type_scope.
Notation := (def (x0 : T) MaybeZero Arbitrary) : type_scope.
Notation := (def x0 MaybeZero EqZero) : type_scope.
Notation := (def x0 NonZero NonNeg) : type_scope.
Notation := (def x0 NonZero NonPos) : type_scope.
Notation := (def x0 MaybeZero NonNeg) : type_scope.
Notation := (def x0 MaybeZero NonPos) : type_scope.
Notation := (def x0 NonZero Real) : type_scope.
Notation := (def x0 MaybeZero Real) : type_scope.
Notation := (def x0 NonZero Arbitrary) : type_scope.
Notation := (def x0 MaybeZero Arbitrary) : type_scope.
Notation := (from (Phantom _ x)) : ring_scope.
Notation := (fromP (Phantom _ x)) : ring_scope.
Notation := r.
Notation := (r x) : ring_scope.
Definition ( : numDomainType) & phant R := {> 0%R : R}.
Notation := (@posnum _ (Phant R))  : ring_scope.
Notation := (@num _ _ 0%R !=0 >=0 x) : ring_scope.
Definition ( : numDomainType) & phant R := {>= 0%R : R}.
Notation := (@nonneg _ (Phant R))  : ring_scope.
Notation := (@num _ _ 0%R ?=0 >=0 x) : ring_scope.
Arguments r {disp T x0 nz cond}.
End Exports.
End Signed.
Export Signed.Exports.

Section POrder.
Variables ( : Order.disp_t) ( : porderType d).
Variables ( : T) ( : nullity) ( : reality).
Local Notation := {compare x0 & nz & cond}.
. for @Signed.r d T x0 nz cond].
..POrder d sT := [POrder of sT by <:].
End POrder.

Lemma ( : porderType d) ( : T) :
  Signed.spec x0 ?=0 >?<0 x.

Proof.

by []. Qed.

Canonical ( : porderType d) ( : T) :=
Signed.Typ (top_typ_subproof x0).

Lemma ( : realDomainType) ( : R) :
Signed.spec 0%R ?=0 >=<0 x.

Proof.

by rewrite /= -realE num_real. Qed.

Canonical ( : realDomainType) :=
Signed.Typ (@real_domain_typ_subproof R).

Lemma ( : realFieldType) ( : R) :
Signed.spec 0%R ?=0 >=<0 x.

Proof.

exact: real_domain_typ_subproof. Qed.

Canonical ( : realFieldType) :=
Signed.Typ (@real_field_typ_subproof R).

Lemma ( : nat) : Signed.spec 0%N ?=0 >=0 x.

Proof.

by []. Qed.

Canonical := Signed.Typ nat_typ_subproof.

Lemma ( : Signed.typ d nz cond)
( : Signed.sort xt) :
Signed.spec (Signed.sort_x0 xt) nz cond x.

Proof.

by move: xt x => []. Qed.

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.

Canonical ( : Signed.typ d nz cond) ( : Signed.sort xt) :=
  Signed.mk (typ_snum_subproof x).

Class {} ( : T) := : f x y = true.
#[global] Hint Mode unify - - - + : typeclass_instances.
Class {} ( : T) := : f x y = true.
#[global] Instance {} ( : T) : unify' f x y -> unify f x y := id.
#[global]
Hint Extern 0 (unify' _ _ _) => vm_compute; reflexivity : typeclass_instances.

Notation nzx nzy :=
  (unify wider_nullity nzx%snum_nullity nzy%snum_nullity).
Notation rx ry :=
  (unify wider_reality rx%snum_sign ry%snum_sign).

#[global] Instance : unify_r (Real AnySign) (Real sign).

Proof.

by []. Qed.

#[global] Instance : unify_r cond =0.

Proof.

by case: cond => [[[]|]|]. Qed.

Section Theory.
Context { : Order.disp_t} { : porderType d} { : T}.
Context { : nullity} { : reality}.
Local Notation := {compare x0 & nz & cond}.
Implicit Type x : sT.

Lemma {} : x%:num = x%:num :> T

Proof.

by []. Qed.

Lemma : unify_nz !=0 nz -> unify_r =0 cond -> False.

Proof.

by move: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= /[swap] ->.
Qed.

Lemma : unify_nz !=0 nz -> unify_r >=0 cond -> x0 < x%:num :> T.

Proof.

move: x => [x /= /andP[]].
by move: cond nz => [[[]|]|] [] //=; rewrite lt_def => -> // /eqP -> /=.
Qed.

Lemma : unify_nz !=0 nz -> unify_r >=0 cond -> x%:num <= x0 :> T = false.

Proof.

by move=> ? ?; rewrite lt_geF//; apply: gt0. Qed.

Lemma : unify_nz !=0 nz -> unify_r <=0 cond -> x%:num < x0 :> T.

Proof.

move: x => [x /= /andP[]].
move: cond nz => [[[]|]|] [] //=; rewrite lt_def [x0 == _]eq_sym => -> //.
by move=> /eqP -> /=.
Qed.

Lemma : unify_nz !=0 nz -> unify_r <=0 cond -> x0 <= x%:num :> T = false.

Proof.

by move=> ? ?; rewrite lt_geF//; apply: lt0. Qed.

Lemma : unify_r >=0 cond -> x0 <= x%:num :> T.

Proof.

by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= _ /eqP ->.
Qed.

Lemma : unify_r >=0 cond -> x%:num < x0 :> T = false.

Proof.

by move=> ?; rewrite le_gtF//; apply: ge0. Qed.

Lemma : unify_r <=0 cond -> x0 >= x%:num :> T.

Proof.

by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= _ /eqP ->.
Qed.

Lemma : unify_r <=0 cond -> x0 < x%:num :> T = false.

Proof.

by move=> ?; rewrite le_gtF//; apply: le0. Qed.

Lemma : unify_r (Real AnySign) cond -> (x0 >=< x%:num).

Proof.

case: x => [x /= /andP[]].
by move: cond nz => [[[]|]|] [] //= _;
do ?[by move=> /eqP ->; rewrite comparablexx];
move=> sx; rewrite /Order.comparable sx// orbT.
Qed.

Lemma : unify_nz !=0 nz -> x%:num != x0 :> T.

Proof.

by case: x => [x /= /andP[]]; move: cond nz => [[[]|]|] []. Qed.

Lemma : unify_nz !=0 nz -> x%:num == x0 :> T = false.

Proof.

by move=> /neq0-/(_ x)/negPf->. Qed.

Lemma : unify_r =0 cond -> x%:num = x0.

Proof.

by case: x => [x /= /andP[_]]; move: cond nz => [[[]|]|] [] //= /eqP ->.
Qed.

Lemma :
unify_nz nz' nz -> unify_r cond' cond ->
Signed.spec x0 nz' cond' x%:num.

Proof.

case: x => [x /= /andP[]].
by case: cond nz cond' nz' => [[[]|]|] [] [[[]|]|] [] //= nz'' cond'';
rewrite ?nz'' ?cond'' ?orbT //; move: cond'' nz'' => /eqP ->; rewrite lexx.
Qed.

Definition
    ( : unify_nz nz' nz) ( : unify_r cond' cond) :=
  Signed.mk (widen_signed_subproof x unz ucond).

Lemma ( : unify_nz nz nz) ( : unify_r cond cond) :
  @widen_signed x nz cond unz ucond = x.

Proof.

exact/val_inj. Qed.

Lemma ( : sT) ( : unify_nz !=0 nz) ( : unify_r >=0 cond) :
(widen_signed x%:num%:sgn unz ucond)%:num = x%:num.

Proof.

by []. Qed.

Lemma ( : sT) ( : unify_nz ?=0 nz) ( : unify_r >=0 cond) :
(widen_signed x%:num%:sgn unz ucond)%:num = x%:num.

Proof.

by []. Qed.

End Theory.

Arguments bottom {d T x0 nz cond} _ {_ _}.
Arguments gt0 {d T x0 nz cond} _ {_ _}.
Arguments le0F {d T x0 nz cond} _ {_ _}.
Arguments lt0 {d T x0 nz cond} _ {_ _}.
Arguments ge0F {d T x0 nz cond} _ {_ _}.
Arguments ge0 {d T x0 nz cond} _ {_}.
Arguments lt0F {d T x0 nz cond} _ {_}.
Arguments le0 {d T x0 nz cond} _ {_}.
Arguments gt0F {d T x0 nz cond} _ {_}.
Arguments cmp0 {d T x0 nz cond} _ {_}.
Arguments neq0 {d T x0 nz cond} _ {_}.
Arguments eq0F {d T x0 nz cond} _ {_}.
Arguments eq0 {d T x0 nz cond} _ {_}.
Arguments widen_signed {d T x0 nz cond} _ {_ _ _ _}.
Arguments widen_signedE {d T x0 nz cond} _ {_ _}.
Arguments posE {d T x0 nz cond} _ {_ _}.
Arguments nngE {d T x0 nz cond} _ {_ _}.

Notation := (ltac:(refine (gt0 x%:sgn))).
Notation := (ltac:(refine (lt0 x%:sgn))).
Notation := (ltac:(refine (ge0 x%:sgn))).
Notation := (ltac:(refine (le0 x%:sgn))).
Notation := (ltac:(refine (cmp0 x%:sgn))).
Notation := (ltac:(refine (neq0 x%:sgn))).

#[global] Hint Extern 0 (is_true (0%R < _)%O) => solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%R)%O) => solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%R <= _)%O) => solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ <= 0%R)%O) => solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (_ \is Num.real)) => solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neq0] : core.

Notation := (widen_signed x%:sgn : {posnum _}) (only parsing)
  : ring_scope.
Notation := (widen_signed x%:sgn : {nonneg _}) (only parsing)
  : ring_scope.
Notation := (@widen_signed _ _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x)) !=0 (Real (Sign >=0)) _ _)
  (only printing) : ring_scope.
Notation := (@widen_signed _ _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x)) ?=0 (Real (Sign >=0)) _ _)
  (only printing) : ring_scope.

Local Open Scope ring_scope.

Section Order.
Variables ( : numDomainType) ( : nullity) ( : real).
Local Notation := {num R & nz & r}.

Lemma : total (<=%O : rel nR).

Proof.

by move=> x y; apply: real_comparable => /=. Qed.

..POrder_isTotal.Build ring_display nR
  signed_le_total.

End Order.

Section POrderStability.
Context { : Order.disp_t} { : porderType disp} { : T}.

Definition ( : nullity) ( : reality) :=
  nz_of_bool
    (xnz && ynz
     || xnz && yr && match xr with Real (Sign <=0) => true | _ => false end
     || ynz && match yr with Real (Sign <=0) => true | _ => false end).
Arguments min_nonzero_subdef /.

Definition ( : nullity) ( : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign >=0), Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign >=0) => >=0
  | Real (Sign <=0), Real _
  | Real _, Real (Sign <=0) => <=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments min_reality_subdef /.

Lemma ( : nullity) ( : reality)
    ( : {compare x0 & xnz & xr}) ( : {compare x0 & ynz & yr})
    ( := min_nonzero_subdef xnz ynz xr yr)
    ( := min_reality_subdef xnz ynz xr yr) :
  Signed.spec x0 rnz rrl (Order.min x%:num y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite /Order.min;
    do ?[by case: (bottom x)|by case: (bottom y)
        |by case: ifP; rewrite ?eq0F// => xlty;
            have := !! lt_trans xlty (lt0 y); rewrite lt_neqAle => /andP[]
        |by rewrite ifT ?eq0F//; apply: lt_le_trans (ge0 y); exact: lt0
        |by have := !! le0 y;
            rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//;
            case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[]].
  have /orP[x0ley|] := !! cmp0 y.
    by rewrite ifT ?eq0F//; apply: lt_le_trans x0ley; exact: lt0.
    rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//.
  by case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[].
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by case: (bottom x)|by case: (bottom y)
      |by apply: comparable_minr; exact: cmp0
      |by rewrite minEle; case: ifP; rewrite ge0
      |by rewrite ?eq0 minEle ?ge0
      |by rewrite ?eq0 minElt; case: ifP; rewrite ?eq0// lt0F
      |by rewrite minEle; case: ifP => [xlty|]; rewrite ?le0//;
          apply: (le_trans xlty); rewrite le0
      |by have /orP[x0ley|] := !! cmp0 y;
          [rewrite minEle ifT ?le0//; apply: le_trans x0ley; exact: le0
          |rewrite minEle; case: ifP => //; exact: le_trans]].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare x0 & xnz & xr}) ( : {compare x0 & ynz & yr}) :=
  Signed.mk (min_snum_subproof x y).

Definition ( : nullity) ( : reality) :=
  nz_of_bool
    (xnz && ynz
     || xnz && match xr with Real (Sign >=0) => true | _ => false end
     || ynz && xr && match yr with Real (Sign >=0) => true | _ => false end).
Arguments max_nonzero_subdef /.

Definition ( : nullity) ( : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign =0) => =0
  | Real (Sign <=0), Real (Sign <=0) => <=0
  | Real (Sign >=0), Real _
  | Real _, Real (Sign >=0) => >=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments max_reality_subdef /.

Lemma ( : nullity) ( : reality)
    ( : {compare x0 & xnz & xr}) ( : {compare x0 & ynz & yr})
    ( := max_nonzero_subdef xnz ynz xr yr)
    ( := max_reality_subdef xnz ynz xr yr) :
  Signed.spec x0 rnz rrl (Order.max x%:num y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite maxElt;
    do ?[by case: (bottom x)|by case: (bottom y)
        |by case: ifP => [xlty|]; rewrite ?eq0F//;
            do [suff : (x0 < y%:num)%O by rewrite lt_def => /andP[]];
            apply: le_lt_trans xlty; exact: ge0
        |by rewrite ifT ?eq0F//; apply: le_lt_trans (gt0 y); exact: le0
        |by have := !! ge0 x;
            rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//;
            case: ifP => _; rewrite ?eq0F// lt_def => /andP[]].
  have /orP[|xlex0] := !! cmp0 x.
    rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//.
    by case: ifP => _; rewrite ?eq0F// lt_def => /andP[].
  by rewrite ifT ?eq0F//; apply: (le_lt_trans xlex0); exact: gt0.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by case: (bottom x)|by case: (bottom y)
      |by apply: comparable_maxr; exact: cmp0
      |by rewrite ?eq0 maxEle ?le0
      |by rewrite ?eq0 maxElt ifF// le_gtF// le0
      |by rewrite maxEle; case: ifP; rewrite ?ge0//; exact/le_trans/ge0
      |by rewrite maxElt; case: ifP => [xlty|]; rewrite ?le0//
      |by have /orP[|xlex0] := !! cmp0 x;
          [rewrite maxEle; case: ifP => // /[swap]; exact: le_trans
          |rewrite maxEle ifT ?ge0//; apply: (le_trans xlex0); exact: ge0]].
Qed.

Canonical ( : nullity) ( : reality)
( : {compare x0 & xnz & xr}) ( : {compare x0 & ynz & yr}) :=
Signed.mk (max_snum_subproof x y).

End POrderStability.

Section NumDomainStability.
Context { : numDomainType}.

Lemma : Signed.spec 0 ?=0 =0 (0 : R).

Proof.

exact: eqxx. Qed.

Canonical := Signed.mk zero_snum_subproof.

Lemma : Signed.spec 0 !=0 >=0 (1 : R).

Proof.

by rewrite /= oner_eq0 ler01. Qed.

Canonical := Signed.mk one_snum_subproof.

Definition ( : nullity) ( : reality) : reality :=
  match xr with
  | Real (Sign =0) => =0
  | Real (Sign >=0) => <=0
  | Real (Sign <=0) => >=0
  | Real AnySign    => >=<0
  | Arbitrary              => >?<0
  end.

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( := opp_reality_subdef xnz xr) :
  Signed.spec 0 xnz r (- x%:num).

Proof.

by rewrite {}/r; case: xr x => [[[]|]|]//= [r]/=;
rewrite oppr_eq0 ?(oppr_ge0, oppr_le0)// orbC.
Qed.

Canonical ( : nullity) ( : reality) ( : {num R & xnz & xr}) :=
  Signed.mk (opp_snum_subproof x).

Definition ( : nullity) ( : reality) :=
  match xr, yr with
  | Real (Sign >=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign =0), Real (Sign =0)
  | Real (Sign >=0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign <=0) => true
  | _, _ => false
  end.

Definition ( : nullity) ( : reality) :=
  nz_of_bool (add_samesign_subdef xnz ynz xr yr && (xnz || ynz)).
Arguments add_nonzero_subdef /.

Definition ( : nullity) ( : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign >=0)
  | Real (Sign >=0), Real (Sign >=0) => >=0
  | Real (Sign <=0), Real (Sign =0)
  | Real (Sign =0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign <=0) => <=0
  | Real _, Real _ => >=<0
  | _, _ => >?<0
  end.
Arguments add_reality_subdef /.

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num R & ynz & yr})
    ( := add_nonzero_subdef xnz ynz xr yr)
    ( := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  by rewrite 1?addr_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
have addr_le0 ( : R) : a <= 0 -> b <= 0 -> a + b <= 0.
  by rewrite -!oppr_ge0 opprD; apply: addr_ge0.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
  do ?[by rewrite addr_ge0|by rewrite addr_le0|by rewrite -realE realD
      |by case: (bottom x)|by case: (bottom y)|by rewrite !eq0 addr0].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num R & ynz & yr}) :=
  Signed.mk (add_snum_subproof x y).

Definition ( : nullity) ( : reality) :=
  nz_of_bool (xnz && ynz).
Arguments mul_nonzero_subdef /.

Definition ( : nullity) ( : reality) : reality :=
  match xr, yr with
  | Real (Sign =0), _ | _, Real (Sign =0) => =0
  | Real (Sign >=0), Real (Sign >=0)
  | Real (Sign <=0), Real (Sign <=0) => >=0
  | Real (Sign >=0), Real (Sign <=0)
  | Real (Sign <=0), Real (Sign >=0) => <=0
  | Real _,          Real _          => >=<0
  | _ , _                            => >?<0
  end.
Arguments mul_reality_subdef /.

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num R & ynz & yr})
    ( := mul_nonzero_subdef xnz ynz xr yr)
    ( := mul_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num * y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
     rewrite mulf_neq0.
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
   do ?[by rewrite mulr_ge0|by rewrite mulr_le0_ge0
       |by rewrite mulr_ge0_le0|by rewrite mulr_le0|by rewrite -realE realM
       |by case: (bottom x)|by case: (bottom y)|by rewrite eq0 ?mulr0// mul0r].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num R & ynz & yr}) :=
  Signed.mk (mul_snum_subproof x y).

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {compare 0%N & nnz & nr})
    ( := mul_nonzero_subdef xnz nnz xr nr)
    ( := mul_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num *+ n%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
     rewrite mulrn_eq0//= ?eq0F.
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)
      |by rewrite mulrn_wge0|by rewrite mulrn_wle0|by rewrite eq0 mul0rn
      |by apply: real_comparable; rewrite ?real0 ?realrMn].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {compare 0%N & nnz & nr}) :=
  Signed.mk (natmul_snum_subproof x n).

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num int & nnz & nr})
    ( := mul_nonzero_subdef xnz nnz xr nr)
    ( := mul_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num *~ n%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
     rewrite mulrz_neq0//= ?neq0.
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x n //;
  do ?[by case: (bottom x)|by case: (bottom n)
      |by rewrite mulrz_ge0|by rewrite mulrz_le0_ge0|by rewrite eq0 mul0rz
      |by rewrite mulrz_ge0_le0|by rewrite mulrz_le0|by rewrite eq0 mulr0z
      |by rewrite -realE rpredMz//; apply: cmp0].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {num int & nnz & nr}) :=
  Signed.mk (intmul_snum_subproof x n).

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) :
  Signed.spec 0 xnz xr (x%:num^-1 : R).

Proof.

by case: xr x => [[[]|]|]//= [r]/=;
rewrite invr_eq0 ?(invr_ge0, invr_le0) ?realV.
Qed.

Canonical ( : nullity) ( : reality) ( : {num R & xnz & xr}) :=
  Signed.mk (inv_snum_subproof x).

Definition ( : nullity)
    ( : reality) : nullity :=
  nz_of_bool (xnz || match nr with Real (Sign =0) => true | _ => false end).
Arguments exprn_nonzero_subdef /.

Definition ( : nullity)
    ( : reality) : reality :=
  match xr, nr with
  | _, Real (Sign =0) => >=0
  | Real (Sign =0), _ => (if nnz then =0 else >=0)%snum_sign
  | Real (Sign >=0), _ => >=0
  | Real _, _ => >=<0
  | _, _ => >?<0
  end.
Arguments exprn_reality_subdef /.

Lemma ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {compare 0%N & nnz & nr})
    ( := exprn_nonzero_subdef xnz nnz xr nr)
    ( := exprn_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num ^+ n%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  by move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
    do ?[by case: (bottom x)|by case: (bottom n)];
    rewrite expf_eq0/= ?eq0// ?eq0F ?andbF//.
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)|by rewrite [_ || _]realX
      |by rewrite eq0 expr0n|exact: exprn_ge0|by rewrite expr0 ler01].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {num R & xnz & xr}) ( : {compare 0%N & nnz & nr}) :=
  Signed.mk (exprn_snum_subproof x n).

Lemma { : normedZmodType R} ( : V) :
  Signed.spec 0 ?=0 >=0 `|x|.

Proof.

by rewrite /=. Qed.

Canonical { : normedZmodType R} ( : V) :=
  Signed.mk (norm_snum_subproof x).

End NumDomainStability.

Section RcfStability.
Context { : rcfType}.

Definition ( : nullity) ( : reality) :=
  if xr is Real (Sign >=0) then xnz else MaybeZero.
Arguments sqrt_nonzero_subdef /.

Lemma ( : {num R & xnz & xr})
    ( := sqrt_nonzero_subdef xnz xr) :
  Signed.spec 0 nz >=0 (Num.sqrt x%:num).

Proof.

by rewrite {}/nz; case: xnz xr x => -[[[]|]|]//= x;
rewrite /= sqrtr_ge0// andbT sqrtr_eq0 le0F.
Qed.

Canonical ( : {num R & xnz & xr}) :=
  Signed.mk (sqrt_snum_subproof x).

End RcfStability.

Section NumClosedStability.
Context { : numClosedFieldType}.

Definition ( : nullity) ( : reality) : reality :=
  match xr with
  | Real (Sign =0) => =0
  | Real (Sign >=0) => >=0
  | _ => >?<0
  end.
Arguments sqrtC_reality_subdef /.

Lemma ( : {num R & xnz & xr})
    ( := sqrtC_reality_subdef xnz xr) :
  Signed.spec 0 xnz r (sqrtC x%:num).

Proof.

rewrite {}/r; apply/andP; split.
by rewrite sqrtC_eq0; case: xr xnz x => [[[]|]|] [] /=.
by case: xr xnz x => [[[]|]|] []//= x; rewrite ?sqrtC_ge0// sqrtC_eq0 eq0.
Qed.

Canonical ( : {num R & xnz & xr}) :=
Signed.mk (sqrtC_snum_subproof x).

End NumClosedStability.

Section NatStability.
Local Open Scope nat_scope.
Implicit Type (n : nat).

Lemma : Signed.spec 0 ?=0 =0 0.

Proof.

by []. Qed.

Canonical := Signed.mk zeron_snum_subproof.

Lemma : Signed.spec 0 !=0 >=0 n.+1.

Proof.

by []. Qed.

Canonical := Signed.mk (succn_snum_subproof n).

Lemma ( : {compare 0 & nz & r}) :
Signed.spec 0 nz r x%:num.*2.

Proof.

by move: nz r x => [] [[[]|]|] [[|n]]. Qed.

Canonical :=
  Signed.mk (@double_snum_subproof nz r x).

Lemma ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr})
    ( := add_nonzero_subdef xnz ynz xr yr)
    ( := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split;
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= [[|x]//= _] [[|y]].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr}) :=
  Signed.mk (addn_snum_subproof x y).

Lemma ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr})
    ( := mul_nonzero_subdef xnz ynz xr yr)
    ( := mul_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num * y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split;
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//=;
by move=> [[|x]//= _] [[|y]//= _]; rewrite muln0.
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr}) :=
  Signed.mk (muln_snum_subproof x y).

Lemma ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & nnz & nr})
    ( := exprn_nonzero_subdef xnz nnz xr nr)
    ( := exprn_reality_subdef xnz nnz xr nr) :
  Signed.spec 0 rnz rrl (x%:num ^ n%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split.
  move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []// x n;
    do ?[by case: (bottom x)|by case: (bottom n)
        |by rewrite ?eq0 ?expn0// expn_eq0 ?eq0F].
move: xr nr xnz nnz x n => [[[]|]|] [[[]|]|] [] []/= x [[|n]//= _] //;
  do ?[by case: (bottom x)|by case: (bottom n)|by rewrite eq0 exp0n].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & nnz & nr}) :=
  Signed.mk (expn_snum_subproof x n).

Lemma ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr})
    ( := min_nonzero_subdef xnz ynz xr yr)
    ( := min_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (min x%:num y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split;
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= [[|x]//= _] [[|y]].
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr}) :=
  Signed.mk (minn_snum_subproof x y).

Lemma ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr})
    ( := max_nonzero_subdef xnz ynz xr yr)
    ( := max_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (maxn x%:num y%:num).

Proof.

rewrite {}/rnz {}/rrl; apply/andP; split;
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//=;
by move=> [[|x]//= _] [[|y]//= _]; rewrite maxnSS.
Qed.

Canonical ( : nullity) ( : reality)
    ( : {compare 0 & xnz & xr}) ( : {compare 0 & ynz & yr}) :=
  Signed.mk (maxn_snum_subproof x y).

End NatStability.

Section IntStability.

Lemma ( : nullity) ( : reality)
    ( : {compare 0%N & xnz & xr}) :
  Signed.spec 0%Z xnz xr (Posz x%:num).

Proof.

by apply/andP; split; move: xr xnz x => [[[]|]|] []//=; move=> [[|x]//= _].
Qed.

Canonical ( : nullity) ( : reality)
( : {compare 0%N & xnz & xr}) :=
Signed.mk (Posz_snum_subproof x).

Lemma ( : nat) : Signed.spec 0%Z !=0 <=0 (Negz n).

Proof.

by []. Qed.

Canonical := Signed.mk (Negz_snum_subproof n).

End IntStability.

Section Morph0.
Context { : numDomainType} { : reality}.
Local Notation := {num R & ?=0 & cond}.
Implicit Types x y : nR.
Local Notation := (@num _ _ (0 : R) ?=0 cond).

Lemma : (x%:num == 0) = (x == (widen_signed 0%:sgn : nR)).

Proof.

by []. Qed.

End Morph0.

Section Morph.
Context { : Order.disp_t} { : porderType d}.
Context { : T} { : nullity} { : reality}.
Local Notation := {compare x0 & nz & cond}.
Implicit Types x y : sT.
Local Notation := (@num _ _ x0 nz cond).

Lemma : {mono num : / x == y}

Proof.

by []. Qed.

Lemma : {mono num : / (x <= y)%O}

Proof.

by []. Qed.

Lemma : {mono num : / (x < y)%O}

Proof.

by []. Qed.

Lemma : {morph num : / Order.min x y}.

Proof.

by move=> x y; rewrite !minEle num_le -fun_if. Qed.

Lemma : {morph num : / Order.max x y}.

Proof.

by move=> x y; rewrite !maxEle num_le -fun_if. Qed.

End Morph.

Section MorphNum.
Context { : numDomainType} { : nullity} { : reality}.
Local Notation := {num R & nz & cond}.
Implicit Types (a : R) (x y : nR).
Local Notation := (@num _ _ (0 : R) nz cond).

Lemma : (`|a|%:nng == 0%:nng) = (a == 0).

Proof.

by rewrite -normr_eq0. Qed.

End MorphNum.

Section MorphReal.
Context { : numDomainType} { : nullity} { : real}.
Local Notation := {num R & nz & r}.
Implicit Type x y : nR.
Local Notation := (@num _ _ (0 : R) nz r).

Lemma :
a <= Num.max x%:num y%:num = (a <= x%:num) || (a <= y%:num).

Proof.

by rewrite -comparable_le_max// real_comparable. Qed.

Lemma :
Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a).

Proof.

by rewrite -comparable_ge_max// real_comparable. Qed.

Lemma :
a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num).

Proof.

by rewrite -comparable_le_min// real_comparable. Qed.

Lemma :
Num.min x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).

Proof.

by rewrite -comparable_ge_min// real_comparable. Qed.

Lemma :
a < Num.max x%:num y%:num = (a < x%:num) || (a < y%:num).

Proof.

by rewrite -comparable_lt_max// real_comparable. Qed.

Lemma :
Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a).

Proof.

by rewrite -comparable_gt_max// real_comparable. Qed.

Lemma :
a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).

Proof.

by rewrite -comparable_lt_min// real_comparable. Qed.

Lemma :
Num.min x%:num y%:num < a = (x%:num < a) || (y%:num < a).

Proof.

by rewrite -comparable_gt_min// real_comparable. Qed.

End MorphReal.

Section MorphGe0.
Context { : numDomainType} { : nullity}.
Local Notation := {num R & ?=0 & >=0}.
Implicit Type x y : nR.
Local Notation := (@num _ _ (0 : R) ?=0 >=0).

Lemma : 0 <= a -> (`|a|%:nng <= x) = (a <= x%:num).

Proof.

by move=> a0; rewrite -num_le//= ger0_norm. Qed.

Lemma : 0 <= a -> (`|a|%:nng < x) = (a < x%:num).

Proof.

by move=> a0; rewrite -num_lt/= ger0_norm. Qed.

End MorphGe0.

Section Posnum.
Context ( : numDomainType) ( : R) ( : 0 < x).
Lemma : (x != 0) && (0 <= x)

Proof.

by rewrite -lt_def. Qed.

Definition : {posnum R} := @Signed.mk _ _ 0 !=0 >=0 _ posnum_subdef.
End Posnum.
Definition ( : numDomainType) ( : R) ( : 0 <= x) : {nonneg R} :=
  (@Signed.mk _ _ 0 ?=0 >=0 x x_ge0).

CoInductive ( : numDomainType) ( : R) :
  R -> bool -> bool -> bool -> Type :=
| ( : {posnum R}) : posnum_spec x (p%:num) false true true.

Lemma ( : numDomainType) ( : R) : 0 < x ->
  posnum_spec x x (x == 0) (0 <= x) (0 < x).

Proof.

move=> x_gt0; case: real_ltgt0P (x_gt0) => []; rewrite ?gtr0_real // => _ _.
by rewrite -[x]/(PosNum x_gt0)%:num; constructor.
Qed.

CoInductive ( : numDomainType) ( : R) : R -> bool -> Type :=
| ( : {nonneg R}) : nonneg_spec x (p%:num) true.

Lemma ( : numDomainType) ( : R) : 0 <= x -> nonneg_spec x x (0 <= x).

Proof.

by move=> xge0; rewrite xge0 -[x]/(NngNum xge0)%:num; constructor. Qed.

These proofs help integrate more arithmetic with signed.v. The issue is Terms like `0 < 1-q` with subtraction don't work well. So we hide the subtractions behind `PosNum` and `NngNum` constructors, see sequences.v for examples.

Section onem_signed.
Variable : numDomainType.
Implicit Types r : R.

Lemma ( : r < 1) : r.~ = (PosNum (onem_gt0 r1))%:num.

Proof.

by []. Qed.

Lemma ( : r <= 1) ( : 0 <= r) :
(r ^+ n).~ = (NngNum (onemX_ge0 n r0 r1))%:num.

Proof.

by []. Qed.

Lemma ( : {nonneg R}) : p%:num <= 1 -> 0 <= (p%:num).~.

Proof.

by rewrite /onem/= subr_ge0. Qed.

Definition ( : {nonneg R}) ( : p%:num <= 1) :=
NngNum (onem_nonneg_proof p1).

End onem_signed.

Files

Module mathcomp.reals.signed