Library mathcomp.algebra.ssrnum

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly.

This file defines some classes to manipulate number structures, i.e structures with an order and a norm. To use this file, insert "Import Num.Theory." before your scripts. You can also "Import Num.Def." to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead of Num.leif, etc.).

NumDomain (Integral domain with an order and a norm)

numDomainType == interface for a num integral domain. NumDomainType T m == packs the num mixin into a numDomainType. The carrier T must have an integral domain and a partial order structures. [numDomainType of T for S] == T-clone of the numDomainType structure S. [numDomainType of T] == clone of a canonical numDomainType structure on T.

NormedZmodule (Zmodule with a norm)

normedZmodType R == interface for a normed Zmodule structure indexed by numDomainType R. NormedZmodType R T m == pack the normed Zmodule mixin into a normedZmodType. The carrier T must have an integral domain structure. [normedZmodType R of T for S] == T-clone of the normedZmodType R structure S. [normedZmodType R of T] == clone of a canonical normedZmodType R structure on T.

NumField (Field with an order and a norm)

numFieldType == interface for a num field. [numFieldType of T] == clone of a canonical numFieldType structure on T.

NumClosedField (Partially ordered Closed Field with conjugation)

numClosedFieldType == interface for a closed field with conj. NumClosedFieldType T r == packs the real closed axiom r into a numClosedFieldType. The carrier T must have a closed field type structure. [numClosedFieldType of T] == clone of a canonical numClosedFieldType structure on T. [numClosedFieldType of T for S] == T-clone of the numClosedFieldType structure S.

RealDomain (Num domain where all elements are positive or negative)

realDomainType == interface for a real integral domain. [realDomainType of T] == clone of a canonical realDomainType structure on T.

RealField (Num Field where all elements are positive or negative)

realFieldType == interface for a real field. [realFieldType of T] == clone of a canonical realFieldType structure on T.

ArchiField (A Real Field with the archimedean axiom)

archiFieldType == interface for an archimedean field. ArchiFieldType T r == packs the archimedean axiom r into an archiFieldType. The carrier T must have a real field type structure. [archiFieldType of T for S] == T-clone of the archiFieldType structure S. [archiFieldType of T] == clone of a canonical archiFieldType structure on T.

RealClosedField (Real Field with the real closed axiom)

rcfType == interface for a real closed field. RcfType T r == packs the real closed axiom r into a rcfType. The carrier T must have a real field type structure. [rcfType of T] == clone of a canonical realClosedFieldType structure on T. [rcfType of T for S] == T-clone of the realClosedFieldType structure S.

The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, _ < _ ?<= if _, >=<, and ><) and lattice operations (meet and join) defined in order.v are redefined for the ring_display in the ring_scope (%R). 0-ary ordering symbols for the ring_display have the suffix "%R", e.g., <%R. All the other ordering notations are the same as order.v.

Over these structures, we have the following operations `|x| == norm of x. Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and to -1 in all other cases (including x < 0). x \is a Num.pos <=> x is positive (:= x > 0). x \is a Num.neg <=> x is negative (:= x < 0). x \is a Num.nneg <=> x is positive or 0 (:= x >= 0). x \is a Num.real <=> x is real (:= x >= 0 or x < 0). Num.bound x == in archimedean fields, and upper bound for x, i.e., and n such that `|x| < n%:R. Num.sqrt x == in a real-closed field, a positive square root of x if x >= 0, or 0 otherwise. For numeric algebraically closed fields we provide the generic definitions 'i == the imaginary number (:= sqrtC (-1)). 'Re z == the real component of z. 'Im z == the imaginary component of z. z^* == the complex conjugate of z (:= conjC z). sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. n.-root z == more generally, for n > 0, an nth root of z, chosen with a minimal non-negative argument for n > 1 (i.e., with a maximal real part subject to a nonnegative imaginary part). Note that n.-root (-1) is a primitive 2nth root of unity, an thus not equal to -1 for n odd > 1 (this will be shown in file cyclotomic.v).

list of prefixes : p : positive n : negative sp : strictly positive sn : strictly negative i : interior = in [0, 1] or ]0, 1[ e : exterior = in [1, +oo[ or ]1; +oo[ w : non strict (weak) monotony

Set Implicit Arguments.

Reserved Notation "n .-root" (at level 2, format "n .-root").
Reserved Notation "'i" (at level 0).
Reserved Notation "'Re z" (at level 10, z at level 8).
Reserved Notation "'Im z" (at level 10, z at level 8).

Local Open Scope order_scope.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory.

Fact ring_display : unit.

Module Num.

Record normed_mixin_of (R T : zmodType)
       (Rorder : Order.POrder.mixin_of (Equality.class R))
       (le_op := Order.POrder.le Rorder)
  := NormedMixin {
  norm_op : T → R;
  _ : ∀ x y, le_op (norm_op (x + y)) (norm_op x + norm_op y);
  _ : ∀ x, norm_op x = 0 → x = 0;
  _ : ∀ x n, norm_op (x *+ n) = norm_op x *+ n;
  _ : ∀ x, norm_op (- x) = norm_op x;
}.

Record mixin_of (R : ringType)
       (Rorder : Order.POrder.mixin_of (Equality.class R))
       (le_op := Order.POrder.le Rorder) (lt_op := Order.POrder.lt Rorder)
       (normed : @normed_mixin_of R R Rorder) (norm_op := norm_op normed)
  := Mixin {
  _ : ∀ x y, lt_op 0 x → lt_op 0 y → lt_op 0 (x + y);
  _ : ∀ x y, le_op 0 x → le_op 0 y → le_op x y || le_op y x;
  _ : {morph norm_op : x y / x × y };
  _ : ∀ x y, (le_op x y ) = (norm_op (y - x) == y - x );
}.

Module NumDomain.

Section ClassDef.
Record class_of T := Class {
  base : GRing.IntegralDomain.class_of T;
  order_mixin : Order.POrder.mixin_of (Equality.class (ring_for T base));
  normed_mixin : normed_mixin_of (ring_for T base) order_mixin;
  mixin : mixin_of normed_mixin;
}.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.
Definition pack (b0 : GRing.IntegralDomain.class_of _) om0
           (nm0 : @normed_mixin_of (ring_for T b0) (ring_for T b0) om0)
           (m0 : @mixin_of (ring_for T b0) om0 nm0) :=
  fun bT (b : GRing.IntegralDomain.class_of T)
      & phant_id (@GRing.IntegralDomain.class bT) b ⇒
  fun om & phant_id om0 om ⇒
  fun nm & phant_id nm0 nm ⇒
  fun m & phant_id m0 m ⇒
  @Pack T (@Class T b om nm m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition porder_zmodType := @GRing.Zmodule.Pack porderType class.
Definition porder_ringType := @GRing.Ring.Pack porderType class.
Definition porder_comRingType := @GRing.ComRing.Pack porderType class.
Definition porder_unitRingType := @GRing.UnitRing.Pack porderType class.
Definition porder_comUnitRingType := @GRing.ComUnitRing.Pack porderType class.
Definition porder_idomainType := @GRing.IntegralDomain.Pack porderType class.

End ClassDef.

Module Exports.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion order_base : class_of >-> Order.POrder.class_of.
Coercion normed_mixin : class_of >-> normed_mixin_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion porderType : type >-> Order.POrder.type.
Canonical porderType.
Canonical porder_zmodType.
Canonical porder_ringType.
Canonical porder_comRingType.
Canonical porder_unitRingType.
Canonical porder_comUnitRingType.
Canonical porder_idomainType.
Notation numDomainType := type.
Notation NumDomainType T m := (@pack T _ _ _ m _ _ id _ id _ id _ id).
Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'numDomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'numDomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'numDomainType' 'of' T ]") : form_scope.
End Exports.

End NumDomain.
Import NumDomain.Exports.

Module NormedZmodule.

Section ClassDef.

Variable R : numDomainType.

Record class_of (T : Type) := Class {
  base : GRing.Zmodule.class_of T;
  mixin : @normed_mixin_of R (@GRing.Zmodule.Pack T base) (NumDomain.class R);
}.

Structure type (phR : phant R) :=
  Pack { sort; _ : class_of sort }.

Variables (phR : phant R) (T : Type) (cT : type phR).

Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Definition pack b0 (m0 : @normed_mixin_of R (@GRing.Zmodule.Pack T b0)
                                          (NumDomain.class R)) :=
  Pack phR (@Class T b0 m0).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Zmodule.class_of.
Coercion mixin : class_of >-> normed_mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Notation normedZmodType R := (type (Phant R)).
Notation NormedZmodType R T m := (@pack _ (Phant R) T _ m).
Notation NormedZmodMixin := Mixin.
Notation "[ 'normedZmodType' R 'of' T 'for' cT ]" :=
  (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'normedZmodType' R 'of' T 'for' cT ]") :
  form_scope.
Notation "[ 'normedZmodType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'normedZmodType' R 'of' T ]") : form_scope.
End Exports.

End NormedZmodule.
Import NormedZmodule.Exports.

Module NumDomain_joins.
Import NumDomain.
Section NumDomain_joins.

Variables (T : Type) (cT : type).

Notation class := (class cT).
Definition normedZmodType : normedZmodType cT :=
  @NormedZmodule.Pack
     cT (Phant cT) cT (NormedZmodule.Class (NumDomain.normed_mixin class)).
Definition normedZmod_ringType := @GRing.Ring.Pack normedZmodType class.
Definition normedZmod_comRingType := @GRing.ComRing.Pack normedZmodType class.
Definition normedZmod_unitRingType := @GRing.UnitRing.Pack normedZmodType class.
Definition normedZmod_comUnitRingType :=
  @GRing.ComUnitRing.Pack normedZmodType class.
Definition normedZmod_idomainType :=
  @GRing.IntegralDomain.Pack normedZmodType class.
Definition normedZmod_porderType :=
  @Order.POrder.Pack ring_display normedZmodType class.

End NumDomain_joins.

Module Exports.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical normedZmod_ringType.
Canonical normedZmod_comRingType.
Canonical normedZmod_unitRingType.
Canonical normedZmod_comUnitRingType.
Canonical normedZmod_idomainType.
Canonical normedZmod_porderType.
End Exports.
End NumDomain_joins.
Export NumDomain_joins.Exports.

Module Import Def.

Definition normr (R : numDomainType) (T : normedZmodType R) : T → R :=
  nosimpl (norm_op (NormedZmodule.class T)).
Arguments normr {R T} x.

Notation ler := (@Order.le ring_display _) (only parsing).
Notation "@ 'ler' R" := (@Order.le ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation ltr := (@Order.lt ring_display _) (only parsing).
Notation "@ 'ltr' R" := (@Order.lt ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation ger := (@Order.ge ring_display _) (only parsing).
Notation "@ 'ger' R" := (@Order.ge ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation gtr := (@Order.gt ring_display _) (only parsing).
Notation "@ 'gtr' R" := (@Order.gt ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation lerif := (@Order.leif ring_display _) (only parsing).
Notation "@ 'lerif' R" := (@Order.leif ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation lterif := (@Order.lteif ring_display _) (only parsing).
Notation "@ 'lteif' R" := (@Order.lteif ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation comparabler := (@Order.comparable ring_display _) (only parsing).
Notation "@ 'comparabler' R" := (@Order.comparable ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation maxr := (@Order.max ring_display _).
Notation "@ 'maxr' R" := (@Order.max ring_display R)
    (at level 10, R at level 8, only parsing) : fun_scope.
Notation minr := (@Order.min ring_display _).
Notation "@ 'minr' R" := (@Order.min ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.

Section Def.
Context {R : numDomainType}.
Implicit Types (x : R).

Definition sgr x : R := if x == 0 then 0 else if x < 0 then -1 else 1.
Definition Rpos : qualifier 0 R := [qualify x : R | 0 < x ].
Definition Rneg : qualifier 0 R := [qualify x : R | x < 0].
Definition Rnneg : qualifier 0 R := [qualify x : R | 0 ≤ x ].
Definition Rreal : qualifier 0 R := [qualify x : R | (0 ≤ x ) || (x ≤ 0)].

End Def. End Def.

Shorter qualified names, when Num.Def is not imported.

Notation norm := normr (only parsing).
Notation le := ler (only parsing).
Notation lt := ltr (only parsing).
Notation ge := ger (only parsing).
Notation gt := gtr (only parsing).
Notation leif := lerif (only parsing).
Notation lteif := lterif (only parsing).
Notation comparable := comparabler (only parsing).
Notation sg := sgr.
Notation max := maxr.
Notation min := minr.
Notation pos := Rpos.
Notation neg := Rneg.
Notation nneg := Rnneg.
Notation real := Rreal.

Module Keys. Section Keys.
Variable R : numDomainType.
Fact Rpos_key : pred_key (@pos R).
Definition Rpos_keyed := KeyedQualifier Rpos_key.
Fact Rneg_key : pred_key (@real R).
Definition Rneg_keyed := KeyedQualifier Rneg_key.
Fact Rnneg_key : pred_key (@nneg R).
Definition Rnneg_keyed := KeyedQualifier Rnneg_key.
Fact Rreal_key : pred_key (@real R).
Definition Rreal_keyed := KeyedQualifier Rreal_key.
End Keys. End Keys.

(Exported) symbolic syntax.

Module Import Syntax.
Import Def Keys.

Notation "`| x |" := (norm x) : ring_scope.

Notation "<=%R" := le : fun_scope.
Notation ">=%R" := ge : fun_scope.
Notation "<%R" := lt : fun_scope.
Notation ">%R" := gt : fun_scope.
Notation "<?=%R" := leif : fun_scope.
Notation "<?<=%R" := lteif : fun_scope.
Notation ">=<%R" := comparable : fun_scope.
Notation "><%R" := (fun x y ⇒ ~~ (comparable x y )) : fun_scope.

Notation "<= y" := (ge y) : ring_scope.
Notation "<= y :> T" := (≤ (y : T)) (only parsing) : ring_scope.
Notation ">= y" := (le y) : ring_scope.
Notation ">= y :> T" := (≥ (y : T)) (only parsing) : ring_scope.

Notation "< y" := (gt y) : ring_scope.
Notation "< y :> T" := (< (y : T)) (only parsing) : ring_scope.
Notation "> y" := (lt y) : ring_scope.
Notation "> y :> T" := (> (y : T)) (only parsing) : ring_scope.

Notation "x <= y" := (le x y) : ring_scope.
Notation "x <= y :> T" := ((x : T) ≤ (y : T)) (only parsing) : ring_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : ring_scope.
Notation "x >= y :> T" := ((x : T) ≥ (y : T)) (only parsing) : ring_scope.

Notation "x < y" := (lt x y) : ring_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : ring_scope.
Notation "x > y" := (y < x) (only parsing) : ring_scope.
Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : ring_scope.

Notation "x <= y <= z" := ((x ≤ y) && (y ≤ z)) : ring_scope.
Notation "x < y <= z" := ((x < y) && (y ≤ z)) : ring_scope.
Notation "x <= y < z" := ((x ≤ y) && (y < z)) : ring_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ring_scope.

Notation "x <= y ?= 'iff' C" := (lerif x y C) : ring_scope.
Notation "x <= y ?= 'iff' C :> R" := ((x : R) ≤ (y : R) ?= iff C)
  (only parsing) : ring_scope.

Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope.
Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C)
  (only parsing) : ring_scope.

Notation ">=< y" := [pred x | comparable x y] : ring_scope.
Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope.
Notation "x >=< y" := (comparable x y) : ring_scope.

Notation ">< y" := [pred x | ~~ comparable x y] : ring_scope.
Notation ">< y :> T" := (>< (y : T)) (only parsing) : ring_scope.
Notation "x >< y" := (~~ (comparable x y)) : ring_scope.

Canonical Rpos_keyed.
Canonical Rneg_keyed.
Canonical Rnneg_keyed.
Canonical Rreal_keyed.

Export Order.POCoercions.

End Syntax.

Section ExtensionAxioms.

Variable R : numDomainType.

Definition real_axiom : Prop := ∀ x : R, x \is real.

Definition archimedean_axiom : Prop := ∀ x : R, ∃ ub , `|x | < ub %:R.

Definition real_closed_axiom : Prop :=
  ∀ (p : {poly R }) (a b : R),
    a ≤ b → p .[a ] ≤ 0 ≤ p .[b ] → exists2 x , a ≤ x ≤ b & root p x.

End ExtensionAxioms.

The rest of the numbers interface hierarchy.

The elementary theory needed to support the definition of the derived operations for the extensions described above.

Module Import Internals.

Section NormedZmodule.
Variables (R : numDomainType) (V : normedZmodType R).
Implicit Types (l : R) (x y : V).

Lemma ler_norm_add x y : `|x + y | ≤ `|x | + `|y |.

Lemma normr0_eq0 x : `|x | = 0 → x = 0.

Lemma normrMn x n : `|x *+ n | = `|x | *+ n.

Lemma normrN x : `|- x | = `|x |.

End NormedZmodule.

Section NumDomain.
Variable R : numDomainType.
Implicit Types x y : R.

Lemmas from the signature

Lemma addr_gt0 x y : 0 < x → 0 < y → 0 < x + y.

Lemma ger_leVge x y : 0 ≤ x → 0 ≤ y → (x ≤ y ) || (y ≤ x ).

Lemma normrM : {morph norm : x y / (x : R ) × y }.

Lemma ler_def x y : (x ≤ y ) = (`|y - x | == y - x ).

Basic consequences (just enough to get predicate closure properties).

Lemma ger0_def x : (0 ≤ x ) = (`|x | == x ).

Lemma subr_ge0 x y : (0 ≤ x - y ) = (y ≤ x ).

Lemma oppr_ge0 x : (0 ≤ - x ) = (x ≤ 0).

Lemma ler01 : 0 ≤ 1 :> R.

Lemma ltr01 : 0 < 1 :> R.

Lemma le0r x : (0 ≤ x ) = (x == 0) || (0 < x ).

Lemma addr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.

Lemma pmulr_rgt0 x y : 0 < x → (0 < x × y ) = (0 < y ).

Closure properties of the real predicates.

Lemma posrE x : (x \is pos ) = (0 < x ).
Lemma nnegrE x : (x \is nneg ) = (0 ≤ x ).
Lemma realE x : (x \is real ) = (0 ≤ x ) || (x ≤ 0).

Fact pos_divr_closed : divr_closed (@pos R).
Canonical pos_mulrPred := MulrPred pos_divr_closed.
Canonical pos_divrPred := DivrPred pos_divr_closed.

Fact nneg_divr_closed : divr_closed (@nneg R).
Canonical nneg_mulrPred := MulrPred nneg_divr_closed.
Canonical nneg_divrPred := DivrPred nneg_divr_closed.

Fact nneg_addr_closed : addr_closed (@nneg R).
Canonical nneg_addrPred := AddrPred nneg_addr_closed.
Canonical nneg_semiringPred := SemiringPred nneg_divr_closed.

Fact real_oppr_closed : oppr_closed (@real R).
Canonical real_opprPred := OpprPred real_oppr_closed.

Fact real_addr_closed : addr_closed (@real R).
Canonical real_addrPred := AddrPred real_addr_closed.
Canonical real_zmodPred := ZmodPred real_oppr_closed.

Fact real_divr_closed : divr_closed (@real R).
Canonical real_mulrPred := MulrPred real_divr_closed.
Canonical real_smulrPred := SmulrPred real_divr_closed.
Canonical real_divrPred := DivrPred real_divr_closed.
Canonical real_sdivrPred := SdivrPred real_divr_closed.
Canonical real_semiringPred := SemiringPred real_divr_closed.
Canonical real_subringPred := SubringPred real_divr_closed.
Canonical real_divringPred := DivringPred real_divr_closed.

End NumDomain.

Lemma num_real (R : realDomainType) (x : R) : x \is real.

Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.

Section RealClosed.
Variable R : rcfType.

Lemma poly_ivt : real_closed_axiom R.

Fact sqrtr_subproof (x : R) :
exists2 y , 0 ≤ y & (if 0 ≤ x then y ^+ 2 == x else y == 0) : bool.

End RealClosed.

End Internals.

Module PredInstances.

Canonical pos_mulrPred.
Canonical pos_divrPred.

Canonical nneg_addrPred.
Canonical nneg_mulrPred.
Canonical nneg_divrPred.
Canonical nneg_semiringPred.

Canonical real_addrPred.
Canonical real_opprPred.
Canonical real_zmodPred.
Canonical real_mulrPred.
Canonical real_smulrPred.
Canonical real_divrPred.
Canonical real_sdivrPred.
Canonical real_semiringPred.
Canonical real_subringPred.
Canonical real_divringPred.

End PredInstances.

Module Import ExtraDef.

Definition archi_bound {R} x := sval (sigW (@archi_bound_subproof R x)).

Definition sqrtr {R} x := s2val (sig2W (@sqrtr_subproof R x)).

End ExtraDef.

Notation bound := archi_bound.
Notation sqrt := sqrtr.

Module Import Theory.

Section NumIntegralDomainTheory.

Variable R : numDomainType.
Implicit Types (V : normedZmodType R) (x y z t : R).

Lemmas from the signature (reexported from internals).

Definition ler_norm_add V (x y : V) : `|x + y | ≤ `|x | + `|y | :=
ler_norm_add x y.
Definition addr_gt0 x y : 0 < x → 0 < y → 0 < x + y := @addr_gt0 R x y.
Definition normr0_eq0 V (x : V) : `|x | = 0 → x = 0 := @normr0_eq0 R V x.
Definition ger_leVge x y : 0 ≤ x → 0 ≤ y → (x ≤ y ) || (y ≤ x ) :=
@ger_leVge R x y.
Definition normrM : {morph norm : x y / (x : R ) × y } := @normrM R.
Definition ler_def x y : (x ≤ y ) = (`|y - x | == y - x ) := ler_def x y.
Definition normrMn V (x : V) n : `|x *+ n | = `|x | *+ n := normrMn x n.
Definition normrN V (x : V) : `|- x | = `|x | := normrN x.

Predicate definitions.

Lemma posrE x : (x \is pos ) = (0 < x ).
Lemma negrE x : (x \is neg ) = (x < 0).
Lemma nnegrE x : (x \is nneg ) = (0 ≤ x ).
Lemma realE x : (x \is real ) = (0 ≤ x ) || (x ≤ 0).

General properties of <= and <

Lemma lt0r x : (0 < x ) = (x != 0) && (0 ≤ x ).
Lemma le0r x : (0 ≤ x ) = (x == 0) || (0 < x ).

Lemma lt0r_neq0 (x : R) : 0 < x → x != 0.

Lemma ltr0_neq0 (x : R) : x < 0 → x != 0.

Lemma pmulr_rgt0 x y : 0 < x → (0 < x × y ) = (0 < y ).

Lemma pmulr_rge0 x y : 0 < x → (0 ≤ x × y ) = (0 ≤ y ).

Integer comparisons and characteristic 0.

Lemma ler01 : 0 ≤ 1 :> R.
Lemma ltr01 : 0 < 1 :> R.
Lemma ler0n n : 0 ≤ n %:R :> R.
Hint Resolve ler01 ltr01 ler0n : core.
Lemma ltr0Sn n : 0 < n .+1 %:R :> R.
Lemma ltr0n n : (0 < n %:R :> R ) = (0 < n)%N.
Hint Resolve ltr0Sn : core.

Lemma pnatr_eq0 n : (n %:R == 0 :> R ) = (n == 0)%N.

Lemma char_num : [char R ] =i pred0.

Properties of the norm.

Lemma ger0_def x : (0 ≤ x ) = (`|x | == x ).
Lemma normr_idP {x} : reflect (`|x | = x) (0 ≤ x).
Lemma ger0_norm x : 0 ≤ x → `|x | = x.
Lemma normr1 : `|1 : R | = 1.
Lemma normr_nat n : `|n %:R : R | = n %:R.

Lemma normr_prod I r (P : pred I) (F : I → R) :
  `|\prod_(i <- r | P i ) F i | = \prod_(i <- r | P i ) `|F i |.

Lemma normrX n x : `|x ^+ n | = `|x | ^+ n.

Lemma normr_unit : {homo (@norm R R ) : x / x \is a GRing.unit }.

Lemma normrV : {in GRing.unit , {morph (@norm R R ) : x / x ^-1 }}.

Lemma normrN1 : `|-1 : R | = 1.

Lemma big_real x0 op I (P : pred I) F (s : seq I) :
  {in real &, ∀ x y, op x y \is real } → x0 \is real →
  {in P , ∀ i, F i \is real } → \big [op /x0 ]_(i <- s | P i ) F i \is real.

Lemma sum_real I (P : pred I) (F : I → R) (s : seq I) :
  {in P , ∀ i, F i \is real } → \sum_(i <- s | P i ) F i \is real.

Lemma prod_real I (P : pred I) (F : I → R) (s : seq I) :
  {in P , ∀ i, F i \is real } → \prod_(i <- s | P i ) F i \is real.

Section NormedZmoduleTheory.

Variable V : normedZmodType R.
Implicit Types (v w : V).

Lemma normr0 : `|0 : V | = 0.

Lemma normr0P v : reflect (`|v | = 0) (v == 0).

Definition normr_eq0 v := sameP (`|v | =P 0) (normr0P v).

Lemma distrC v w : `|v - w | = `|w - v |.

Lemma normr_id v : `| `|v | | = `|v |.

Lemma normr_ge0 v : 0 ≤ `|v |.

Lemma normr_le0 v : `|v | ≤ 0 = (v == 0).

Lemma normr_lt0 v : `|v | < 0 = false.

Lemma normr_gt0 v : `|v | > 0 = (v != 0).

Definition normrE := (normr_id , normr0 , normr1 , normrN1 , normr_ge0 , normr_eq0 ,
  normr_lt0 , normr_le0 , normr_gt0 , normrN ).

End NormedZmoduleTheory.

Lemma ler0_def x : (x ≤ 0) = (`|x | == - x ).

Lemma ler0_norm x : x ≤ 0 → `|x | = - x.

Definition gtr0_norm x (hx : 0 < x) := ger0_norm (ltW hx).
Definition ltr0_norm x (hx : x < 0) := ler0_norm (ltW hx).

Comparision to 0 of a difference

Lemma subr_ge0 x y : (0 ≤ y - x ) = (x ≤ y ).
Lemma subr_gt0 x y : (0 < y - x ) = (x < y ).
Lemma subr_le0 x y : (y - x ≤ 0) = (y ≤ x ).
Lemma subr_lt0 x y : (y - x < 0) = (y < x ).

Definition subr_lte0 := (subr_le0 , subr_lt0 ).
Definition subr_gte0 := (subr_ge0 , subr_gt0 ).
Definition subr_cp0 := (subr_lte0 , subr_gte0 ).

Comparability in a numDomain

Lemma comparable0r x : (0 >=< x)%R = (x \is Num.real ).

Lemma comparabler0 x : (x >=< 0)%R = (x \is Num.real ).

Lemma subr_comparable0 x y : (x - y >=< 0)%R = (x >=< y)%R.

Lemma comparablerE x y : (x >=< y)%R = (x - y \is Num.real ).

Lemma comparabler_trans : transitive (comparable : rel R).

Ordered ring properties.

Definition lter01 := (ler01 , ltr01 ).

Lemma addr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.

End NumIntegralDomainTheory.

Arguments ler01 {R}.
Arguments ltr01 {R}.
Arguments normr_idP {R x}.
Arguments normr0P {R V v}.
#[global] Hint Resolve ler01 ltr01 ltr0Sn ler0n : core.
#[global] Hint Extern 0 (is_true (0 ≤ norm _)) ⇒ apply: normr_ge0 : core.

Lemma normr_nneg (R : numDomainType) (x : R) : `|x | \is Num.nneg.
#[global] Hint Resolve normr_nneg : core.

Section NumDomainOperationTheory.

Variable R : numDomainType.
Implicit Types x y z t : R.

Comparision and opposite.

Lemma ler_opp2 : {mono -%R : x y /~ x ≤ y :> R }.
Hint Resolve ler_opp2 : core.
Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R }.
Hint Resolve ltr_opp2 : core.
Definition lter_opp2 := (ler_opp2 , ltr_opp2 ).

Lemma ler_oppr x y : (x ≤ - y ) = (y ≤ - x ).

Lemma ltr_oppr x y : (x < - y ) = (y < - x ).

Definition lter_oppr := (ler_oppr , ltr_oppr ).

Lemma ler_oppl x y : (- x ≤ y ) = (- y ≤ x ).

Lemma ltr_oppl x y : (- x < y ) = (- y < x ).

Definition lter_oppl := (ler_oppl , ltr_oppl ).

Lemma oppr_ge0 x : (0 ≤ - x ) = (x ≤ 0).

Lemma oppr_gt0 x : (0 < - x ) = (x < 0).

Definition oppr_gte0 := (oppr_ge0 , oppr_gt0 ).

Lemma oppr_le0 x : (- x ≤ 0) = (0 ≤ x ).

Lemma oppr_lt0 x : (- x < 0) = (0 < x ).

Lemma gtr_opp x : 0 < x → - x < x.

Definition oppr_lte0 := (oppr_le0 , oppr_lt0 ).
Definition oppr_cp0 := (oppr_gte0 , oppr_lte0 ).
Definition lter_oppE := (oppr_cp0 , lter_opp2 ).

Lemma ge0_cp x : 0 ≤ x → (- x ≤ 0) × (- x ≤ x ).

Lemma gt0_cp x : 0 < x →
(0 ≤ x ) × (- x ≤ 0) × (- x ≤ x ) × (- x < 0) × (- x < x ).

Lemma le0_cp x : x ≤ 0 → (0 ≤ - x ) × (x ≤ - x ).

Lemma lt0_cp x :
x < 0 → (x ≤ 0) × (0 ≤ - x ) × (x ≤ - x ) × (0 < - x ) × (x < - x ).

Properties of the real subset.

Lemma ger0_real x : 0 ≤ x → x \is real.

Lemma ler0_real x : x ≤ 0 → x \is real.

Lemma gtr0_real x : 0 < x → x \is real.

Lemma ltr0_real x : x < 0 → x \is real.

Lemma real0 : 0 \is @real R.
Hint Resolve real0 : core.

Lemma real1 : 1 \is @real R.
Hint Resolve real1 : core.

Lemma realn n : n %:R \is @real R.

Lemma ler_leVge x y : x ≤ 0 → y ≤ 0 → (x ≤ y ) || (y ≤ x ).

Lemma real_leVge x y : x \is real → y \is real → (x ≤ y ) || (y ≤ x ).

Lemma real_comparable x y : x \is real → y \is real → x >=< y.

Lemma realB : {in real &, ∀ x y, x - y \is real }.

Lemma realN : {mono (@GRing.opp R ) : x / x \is real }.

Lemma realBC x y : (x - y \is real ) = (y - x \is real ).

Lemma realD : {in real &, ∀ x y, x + y \is real }.

dichotomy and trichotomy

Variant ler_xor_gt (x y : R) : R → R → R → R → R → R →
    bool → bool → Set :=
  | LerNotGt of x ≤ y : ler_xor_gt x y x x y y (y - x) (y - x) true false
  | GtrNotLe of y < x : ler_xor_gt x y y y x x (x - y) (x - y) false true.

Variant ltr_xor_ge (x y : R) : R → R → R → R → R → R →
    bool → bool → Set :=
  | LtrNotGe of x < y : ltr_xor_ge x y x x y y (y - x) (y - x) false true
  | GerNotLt of y ≤ x : ltr_xor_ge x y y y x x (x - y) (x - y) true false.

Variant comparer x y : R → R → R → R → R → R →
    bool → bool → bool → bool → bool → bool → Set :=
  | ComparerLt of x < y : comparer x y x x y y (y - x) (y - x)
    false false false true false true
  | ComparerGt of x > y : comparer x y y y x x (x - y) (x - y)
    false false true false true false
  | ComparerEq of x = y : comparer x y x x x x 0 0
    true true true true false false.

Lemma real_leP x y : x \is real → y \is real →
  ler_xor_gt x y (min y x) (min x y) (max y x) (max x y)
                 `|x - y | `|y - x | (x ≤ y) (y < x).

Lemma real_ltP x y : x \is real → y \is real →
  ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y)
             `|x - y | `|y - x | (y ≤ x) (x < y).

Lemma real_ltNge : {in real &, ∀ x y, (x < y ) = ~~ (y ≤ x )}.

Lemma real_leNgt : {in real &, ∀ x y, (x ≤ y ) = ~~ (y < x )}.

Lemma real_ltgtP x y : x \is real → y \is real →
  comparer x y (min y x) (min x y) (max y x) (max x y) `|x - y | `|y - x |
               (y == x) (x == y) (x ≥ y) (x ≤ y) (x > y) (x < y).

Variant ger0_xor_lt0 (x : R) : R → R → R → R → R →
    bool → bool → Set :=
  | Ger0NotLt0 of 0 ≤ x : ger0_xor_lt0 x 0 0 x x x false true
  | Ltr0NotGe0 of x < 0 : ger0_xor_lt0 x x x 0 0 (- x) true false.

Variant ler0_xor_gt0 (x : R) : R → R → R → R → R →
   bool → bool → Set :=
  | Ler0NotLe0 of x ≤ 0 : ler0_xor_gt0 x x x 0 0 (- x) false true
  | Gtr0NotGt0 of 0 < x : ler0_xor_gt0 x 0 0 x x x true false.

Variant comparer0 x : R → R → R → R → R →
    bool → bool → bool → bool → bool → bool → Set :=
  | ComparerGt0 of 0 < x : comparer0 x 0 0 x x x false false false true false true
  | ComparerLt0 of x < 0 : comparer0 x x x 0 0 (- x) false false true false true false
  | ComparerEq0 of x = 0 : comparer0 x 0 0 0 0 0 true true true true false false.

Lemma real_ge0P x : x \is real → ger0_xor_lt0 x
   (min 0 x) (min x 0) (max 0 x) (max x 0)
  `|x | (x < 0) (0 ≤ x).

Lemma real_le0P x : x \is real → ler0_xor_gt0 x
  (min 0 x) (min x 0) (max 0 x) (max x 0)
  `|x | (0 < x) (x ≤ 0).

Lemma real_ltgt0P x : x \is real →
  comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0)
            `|x | (0 == x) (x == 0) (x ≤ 0) (0 ≤ x) (x < 0) (x > 0).

Lemma max_real : {in real &, ∀ x y, max x y \is real }.

Lemma min_real : {in real &, ∀ x y, min x y \is real }.

Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I → R):
  x0 \is real → {in P , ∀ i : I, f i \is real } →
  \big [max /x0 ]_(i <- r | P i ) f i \is real.

Lemma bigmin_real I x0 (r : seq I) (P : pred I) (f : I → R):
  x0 \is real → {in P , ∀ i : I, f i \is real } →
  \big [min /x0 ]_(i <- r | P i ) f i \is real.

Lemma real_neqr_lt : {in real &, ∀ x y, (x != y ) = (x < y ) || (y < x )}.

Lemma ler_sub_real x y : x ≤ y → y - x \is real.

Lemma ger_sub_real x y : x ≤ y → x - y \is real.

Lemma ler_real y x : x ≤ y → (x \is real ) = (y \is real ).

Lemma ger_real x y : y ≤ x → (x \is real ) = (y \is real ).

Lemma ger1_real x : 1 ≤ x → x \is real.
Lemma ler1_real x : x ≤ 1 → x \is real.

Lemma Nreal_leF x y : y \is real → x \notin real → (x ≤ y ) = false.

Lemma Nreal_geF x y : y \is real → x \notin real → (y ≤ x ) = false.

Lemma Nreal_ltF x y : y \is real → x \notin real → (x < y ) = false.

Lemma Nreal_gtF x y : y \is real → x \notin real → (y < x ) = false.

real wlog

Lemma real_wlog_ler P :
    (∀ a b, P b a → P a b ) → (∀ a b, a ≤ b → P a b ) →
  ∀ a b : R, a \is real → b \is real → P a b.

Lemma real_wlog_ltr P :
    (∀ a, P a a ) → (∀ a b, (P b a → P a b)) →
    (∀ a b, a < b → P a b ) →
  ∀ a b : R, a \is real → b \is real → P a b.

Monotony of addition

Lemma ler_add2l x : {mono +%R x : y z / y ≤ z }.

Lemma ler_add2r x : {mono +%R ^~ x : y z / y ≤ z }.

Lemma ltr_add2l x : {mono +%R x : y z / y < z }.

Lemma ltr_add2r x : {mono +%R ^~ x : y z / y < z }.

Definition ler_add2 := (ler_add2l , ler_add2r ).
Definition ltr_add2 := (ltr_add2l , ltr_add2r ).
Definition lter_add2 := (ler_add2 , ltr_add2 ).

Addition, subtraction and transitivity

Lemma ler_add x y z t : x ≤ y → z ≤ t → x + z ≤ y + t.

Lemma ler_lt_add x y z t : x ≤ y → z < t → x + z < y + t.

Lemma ltr_le_add x y z t : x < y → z ≤ t → x + z < y + t.

Lemma ltr_add x y z t : x < y → z < t → x + z < y + t.

Lemma ler_sub x y z t : x ≤ y → t ≤ z → x - z ≤ y - t.

Lemma ler_lt_sub x y z t : x ≤ y → t < z → x - z < y - t.

Lemma ltr_le_sub x y z t : x < y → t ≤ z → x - z < y - t.

Lemma ltr_sub x y z t : x < y → t < z → x - z < y - t.

Lemma ler_subl_addr x y z : (x - y ≤ z ) = (x ≤ z + y ).

Lemma ltr_subl_addr x y z : (x - y < z ) = (x < z + y ).

Lemma ler_subr_addr x y z : (x ≤ y - z ) = (x + z ≤ y ).

Lemma ltr_subr_addr x y z : (x < y - z ) = (x + z < y ).

Definition ler_sub_addr := (ler_subl_addr , ler_subr_addr ).
Definition ltr_sub_addr := (ltr_subl_addr , ltr_subr_addr ).
Definition lter_sub_addr := (ler_sub_addr , ltr_sub_addr ).

Lemma ler_subl_addl x y z : (x - y ≤ z ) = (x ≤ y + z ).

Lemma ltr_subl_addl x y z : (x - y < z ) = (x < y + z ).

Lemma ler_subr_addl x y z : (x ≤ y - z ) = (z + x ≤ y ).

Lemma ltr_subr_addl x y z : (x < y - z ) = (z + x < y ).

Definition ler_sub_addl := (ler_subl_addl , ler_subr_addl ).
Definition ltr_sub_addl := (ltr_subl_addl , ltr_subr_addl ).
Definition lter_sub_addl := (ler_sub_addl , ltr_sub_addl ).

Lemma ler_addl x y : (x ≤ x + y ) = (0 ≤ y ).

Lemma ltr_addl x y : (x < x + y ) = (0 < y ).

Lemma ler_addr x y : (x ≤ y + x ) = (0 ≤ y ).

Lemma ltr_addr x y : (x < y + x ) = (0 < y ).

Lemma ger_addl x y : (x + y ≤ x ) = (y ≤ 0).

Lemma gtr_addl x y : (x + y < x ) = (y < 0).

Lemma ger_addr x y : (y + x ≤ x ) = (y ≤ 0).

Lemma gtr_addr x y : (y + x < x ) = (y < 0).

Definition cpr_add := (ler_addl , ler_addr , ger_addl , ger_addl ,
ltr_addl , ltr_addr , gtr_addl , gtr_addl ).

Addition with left member knwon to be positive/negative

Lemma ler_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.

Lemma ltr_paddl y x z : 0 ≤ x → y < z → y < x + z.

Lemma ltr_spaddl y x z : 0 < x → y ≤ z → y < x + z.

Lemma ltr_spsaddl y x z : 0 < x → y < z → y < x + z.

Lemma ler_naddl y x z : x ≤ 0 → y ≤ z → x + y ≤ z.

Lemma ltr_naddl y x z : x ≤ 0 → y < z → x + y < z.

Lemma ltr_snaddl y x z : x < 0 → y ≤ z → x + y < z.

Lemma ltr_snsaddl y x z : x < 0 → y < z → x + y < z.

Addition with right member we know positive/negative

Lemma ler_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.

Lemma ltr_paddr y x z : 0 ≤ x → y < z → y < z + x.

Lemma ltr_spaddr y x z : 0 < x → y ≤ z → y < z + x.

Lemma ltr_spsaddr y x z : 0 < x → y < z → y < z + x.

Lemma ler_naddr y x z : x ≤ 0 → y ≤ z → y + x ≤ z.

Lemma ltr_naddr y x z : x ≤ 0 → y < z → y + x < z.

Lemma ltr_snaddr y x z : x < 0 → y ≤ z → y + x < z.

Lemma ltr_snsaddr y x z : x < 0 → y < z → y + x < z.

x and y have the same sign and their sum is null

Lemma paddr_eq0 (x y : R) :
  0 ≤ x → 0 ≤ y → (x + y == 0) = (x == 0) && (y == 0).

Lemma naddr_eq0 (x y : R) :
  x ≤ 0 → y ≤ 0 → (x + y == 0) = (x == 0) && (y == 0).

Lemma addr_ss_eq0 (x y : R) :
    (0 ≤ x ) && (0 ≤ y ) || (x ≤ 0) && (y ≤ 0) →
  (x + y == 0) = (x == 0) && (y == 0).

big sum and ler

Lemma sumr_ge0 I (r : seq I) (P : pred I) (F : I → R) :
  (∀ i, P i → (0 ≤ F i )) → 0 ≤ \sum_(i <- r | P i ) (F i ).

Lemma ler_sum I (r : seq I) (P : pred I) (F G : I → R) :
    (∀ i, P i → F i ≤ G i ) →
  \sum_(i <- r | P i ) F i ≤ \sum_(i <- r | P i ) G i.

Lemma ler_sum_nat (m n : nat) (F G : nat → R) :
  (∀ i, (m ≤ i < n)%N → F i ≤ G i ) →
  \sum_(m ≤ i < n ) F i ≤ \sum_(m ≤ i < n ) G i.

Lemma psumr_eq0 (I : eqType) (r : seq I) (P : pred I) (F : I → R) :
    (∀ i, P i → 0 ≤ F i ) →
  (\sum_(i <- r | P i ) (F i ) == 0) = (all (fun i ⇒ (P i ) ==> (F i == 0)) r ).

:TODO: Cyril : See which form to keep

Lemma psumr_eq0P (I : finType) (P : pred I) (F : I → R) :
     (∀ i, P i → 0 ≤ F i ) → \sum_(i | P i ) F i = 0 →
  (∀ i, P i → F i = 0).

Lemma psumr_neq0 (I : eqType) (r : seq I) (P : pred I) (F : I → R) :
    (∀ i, P i → 0 ≤ F i ) →
  (\sum_(i <- r | P i ) (F i ) != 0) = (has (fun i ⇒ P i && (0 < F i )) r ).

Lemma psumr_neq0P (I : finType) (P : pred I) (F : I → R) :
     (∀ i, P i → 0 ≤ F i ) → \sum_(i | P i ) F i ≠ 0 →
  (∃ i , P i && (0 < F i )).

mulr and ler/ltr

Lemma ler_pmul2l x : 0 < x → {mono *%R x : x y / x ≤ y }.

Lemma ltr_pmul2l x : 0 < x → {mono *%R x : x y / x < y }.

Definition lter_pmul2l := (ler_pmul2l , ltr_pmul2l ).

Lemma ler_pmul2r x : 0 < x → {mono *%R ^~ x : x y / x ≤ y }.

Lemma ltr_pmul2r x : 0 < x → {mono *%R ^~ x : x y / x < y }.

Definition lter_pmul2r := (ler_pmul2r , ltr_pmul2r ).

Lemma ler_nmul2l x : x < 0 → {mono *%R x : x y /~ x ≤ y }.

Lemma ltr_nmul2l x : x < 0 → {mono *%R x : x y /~ x < y }.

Definition lter_nmul2l := (ler_nmul2l , ltr_nmul2l ).

Lemma ler_nmul2r x : x < 0 → {mono *%R ^~ x : x y /~ x ≤ y }.

Lemma ltr_nmul2r x : x < 0 → {mono *%R ^~ x