Library mathcomp.algebra.ssrnum
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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.
Number structures
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
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.).
This file defines the following number structures:
porderZmodType == join of Order.POrder and GRing.Zmodule
The HB class is called POrderedZmodule.
normedZmodType == Zmodule with a norm
The HB class is called NormedZmodule.
numDomainType == Integral domain with an order and a norm
The HB class is called NumDomain.
numFieldType == Field with an order and a norm
The HB class is called NumField.
numClosedFieldType == Partially ordered Closed Field with conjugation
The HB class is called ClosedField.
realDomainType == Num domain where all elements are positive or negative
The HB class is called RealDomain.
realFieldType == Num Field where all elements are positive or negative
The HB class is called RealField.
rcfType == A Real Field with the real closed axiom
The HB class is called RealClosedField.
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.npos <=> x is negative or 0 (:= x <= 0)
x \is a Num.real <=> x is real (:= x >= 0 or x < 0)
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 : Order.disp_t.
Module Num.
#[short(type="porderZmodType")]
HB.structure Definition POrderedZmodule :=
{ R of Order.isPOrder ring_display R & GRing.Zmodule R }.
#[short(type="normedZmodType")]
HB.structure Definition NormedZmodule (R : porderZmodType) :=
{ M of Zmodule_isNormed R M & GRing.Zmodule M }.
Arguments norm {R M} x : rename.
Module NormedZmoduleExports.
Bind Scope ring_scope with NormedZmodule.sort.
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 NormedZmoduleExports.
#[short(type="numDomainType")]
HB.structure Definition NumDomain := { R of
GRing.IntegralDomain R &
POrderedZmodule R &
NormedZmodule (POrderedZmodule.clone R _) R &
isNumRing R
}.
Arguments addr_gt0 {_} [x y] : rename.
Arguments ger_leVge {_} [x y] : rename.
#[short(type="numDomainType")]
HB.structure Definition NumDomain := { R of
GRing.IntegralDomain R &
POrderedZmodule R &
NormedZmodule (POrderedZmodule.clone R _) R &
isNumRing R
}.
Arguments addr_gt0 {_} [x y] : rename.
Arguments ger_leVge {_} [x y] : rename.
TODO: make isNumDomain depend on intermediate structures
TODO: make isNumDomain.sort canonically a NumDomain
Module NumDomainExports.
Bind Scope ring_scope with NumDomain.sort.
End NumDomainExports.
Module Import Def.
Notation normr := norm.
Notation "`| x |" := (norm x) : ring_scope.
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) : function_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) : function_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) : function_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) : function_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) : function_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) : function_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) : function_scope.
Notation maxr := (@Order.max ring_display _).
Notation "@ 'maxr' R" := (@Order.max ring_display R)
(at level 10, R at level 8, only parsing) : function_scope.
Notation minr := (@Order.min ring_display _).
Notation "@ 'minr' R" := (@Order.min ring_display R)
(at level 10, R at level 8, only parsing) : function_scope.
Section NumDomainDef.
Context {R : numDomainType}.
Definition sgr (x : R) : R := if x == 0 then 0 else if x < 0 then -1 else 1.
Definition Rpos_pred := fun x : R ⇒ 0 < x.
Definition Rpos : qualifier 0 R := [qualify x | Rpos_pred x].
Definition Rneg_pred := fun x : R ⇒ x < 0.
Definition Rneg : qualifier 0 R := [qualify x : R | Rneg_pred x].
Definition Rnneg_pred := fun x : R ⇒ 0 ≤ x.
Definition Rnneg : qualifier 0 R := [qualify x : R | Rnneg_pred x].
Definition Rnpos_pred := fun x : R ⇒ x ≤ 0.
Definition Rnpos : qualifier 0 R := [qualify x : R | Rnpos_pred x].
Definition Rreal_pred := fun x : R ⇒ (0 ≤ x) || (x ≤ 0).
Definition Rreal : qualifier 0 R := [qualify x : R | Rreal_pred x].
End NumDomainDef.
End Def.
Arguments Rpos_pred _ _ /.
Arguments Rneg_pred _ _ /.
Arguments Rnneg_pred _ _ /.
Arguments Rreal_pred _ _ /.
Shorter qualified names, when Num.Def is not imported.
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 npos := Rnpos.
Notation real := Rreal.
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 npos := Rnpos.
Notation real := Rreal.
(Exported) symbolic syntax.
Module Import Syntax.
Import Def.
Notation "`| x |" := (norm x) : ring_scope.
Notation "<=%R" := le : function_scope.
Notation ">=%R" := ge : function_scope.
Notation "<%R" := lt : function_scope.
Notation ">%R" := gt : function_scope.
Notation "<?=%R" := leif : function_scope.
Notation "<?<=%R" := lteif : function_scope.
Notation ">=<%R" := comparable : function_scope.
Notation "><%R" := (fun x y ⇒ ~~ (comparable x y)) : function_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.
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.
Import Def.
Notation "`| x |" := (norm x) : ring_scope.
Notation "<=%R" := le : function_scope.
Notation ">=%R" := ge : function_scope.
Notation "<%R" := lt : function_scope.
Notation ">%R" := gt : function_scope.
Notation "<?=%R" := leif : function_scope.
Notation "<?<=%R" := lteif : function_scope.
Notation ">=<%R" := comparable : function_scope.
Notation "><%R" := (fun x y ⇒ ~~ (comparable x y)) : function_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.
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.
#[short(type="numFieldType")]
HB.structure Definition NumField := { R of GRing.UnitRing_isField R &
GRing.IntegralDomain R &
POrderedZmodule R &
NormedZmodule (POrderedZmodule.clone R _) R &
isNumRing R }.
Module NumFieldExports.
Bind Scope ring_scope with NumField.sort.
End NumFieldExports.
#[short(type="numClosedFieldType")]
HB.structure Definition ClosedField :=
{ R of NumField_isImaginary R & GRing.ClosedField R & NumField R }.
Module ClosedFieldExports.
Bind Scope ring_scope with ClosedField.sort.
End ClosedFieldExports.
#[short(type="realDomainType")]
HB.structure Definition RealDomain :=
{ R of Order.Total ring_display R & NumDomain R }.
Module RealDomainExports.
Bind Scope ring_scope with RealDomain.sort.
End RealDomainExports.
#[short(type="realFieldType")]
HB.structure Definition RealField :=
{ R of Order.Total