Module mathcomp.algebra.archimedean
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop nmodule order.
From mathcomp Require Import rings_modules_and_algebras divalg decfield poly.
From mathcomp Require Import orderedzmod numdomain numfield ssrint.
Archimedean structures
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
This file defines some numeric structures extended with the Archimedean
axiom. To use this file, insert "Import Num.Theory." and optionally
"Import Num.Def." before your scripts as in the ssrnum library.
The modules provided by this library subsume those from ssrnum.
This file defines the following structures:
archiNumDomainType == numDomainType with the Archimedean axiom
The HB class is called ArchiNumDomain.
archiNumFieldType == numFieldType with the Archimedean axiom
The HB class is called ArchiNumField.
archiClosedFieldType == closedFieldType with the Archimedean axiom
The HB class is called ArchiClosedField.
archiRealDomainType == realDomainType with the Archimedean axiom
The HB class is called ArchiRealDomain.
archiRealFieldType == realFieldType with the Archimedean axiom
The HB class is called ArchiRealField.
archiRcfType == rcfType with the Archimedean axiom
The HB class is called ArchiRealClosedField.
Over these structures, we have the following operations:
x \is a Num.int <=> x is an integer, i.e., x = m%:~R for some m : int
x \is a Num.nat <=> x is a natural number, i.e., x = m%:R for some m : nat
Num.floor x == the m : int such that m%:~R <= x < (m + 1)%:~R
when x \is a Num.real, otherwise 0%Z
Num.ceil x == the m : int such that (m - 1)%:~R < x <= m%:~R
when x \is a Num.real, otherwise 0%Z
Num.truncn x == the n : nat such that n%:R <= x < n.+1%:R
when 0 <= n, otherwise 0%N
Num.bound x == an upper bound for x, i.e., an n such that `|x| < n%:R
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Module Num.
Import Num.Def.
HB.mixin Record NumDomain_hasFloorCeilTruncn R & Num.NumDomain R := {
floor : R -> int;
ceil : R -> int;
truncn : R -> nat;
int_num_subdef : pred R;
nat_num_subdef : pred R;
floor_subproof :
forall x,
if x \is real_num then (floor x)%:~R <= x < (floor x + 1)%:~R
else floor x == 0;
ceil_subproof : forall x, ceil x = - floor (- x);
truncn_subproof : forall x, truncn x = if floor x is Posz n then n else 0;
int_num_subproof : forall x, reflect (exists n, x = n%:~R) (int_num_subdef x);
nat_num_subproof : forall x, reflect (exists n, x = n%:R) (nat_num_subdef x);
}.
#[short(type="archiNumDomainType")]
HB.structure Definition ArchiNumDomain :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.NumDomain R }.
Module ArchiNumDomainExports.
Bind Scope ring_scope with ArchiNumDomain.sort.
End ArchiNumDomainExports.
HB.export ArchiNumDomainExports.
#[short(type="archiNumFieldType")]
HB.structure Definition ArchiNumField :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.NumField R }.
Module ArchiNumFieldExports.
Bind Scope ring_scope with ArchiNumField.sort.
End ArchiNumFieldExports.
HB.export ArchiNumFieldExports.
#[short(type="archiClosedFieldType")]
HB.structure Definition ArchiClosedField :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.ClosedField R }.
Module ArchiClosedFieldExports.
Bind Scope ring_scope with ArchiClosedField.sort.
End ArchiClosedFieldExports.
HB.export ArchiClosedFieldExports.
#[short(type="archiRealDomainType")]
HB.structure Definition ArchiRealDomain :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.RealDomain R }.
Module ArchiRealDomainExports.
Bind Scope ring_scope with ArchiRealDomain.sort.
End ArchiRealDomainExports.
HB.export ArchiRealDomainExports.
#[short(type="archiRealFieldType")]
HB.structure Definition ArchiRealField :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.RealField R }.
Module ArchiRealFieldExports.
Bind Scope ring_scope with ArchiRealField.sort.
End ArchiRealFieldExports.
HB.export ArchiRealFieldExports.
#[short(type="archiRcfType")]
HB.structure Definition ArchiRealClosedField :=
{ R of NumDomain_hasFloorCeilTruncn R & Num.RealClosedField R }.
Module ArchiRealClosedFieldExports.
Bind Scope ring_scope with ArchiRealClosedField.sort.
End ArchiRealClosedFieldExports.
HB.export ArchiRealClosedFieldExports.
Section Def.
Context {R : archiNumDomainType}.
Definition nat_num : qualifier 1 R := [qualify a x : R | nat_num_subdef x].
Definition int_num : qualifier 1 R := [qualify a x : R | int_num_subdef x].
Definition bound (x : R) := (truncn `|x|).+1.
End Def.
Arguments floor {R} : rename, simpl never.
Arguments ceil {R} : rename, simpl never.
Arguments truncn {R} : rename, simpl never.
Arguments nat_num {R} : simpl never.
Arguments int_num {R} : simpl never.
#[deprecated(since="mathcomp 2.4.0", use=truncn)]
Notation trunc := truncn (only parsing).
Module Def.
Export Num.Def.
Notation truncn := truncn.
#[deprecated(since="mathcomp 2.4.0", use=truncn)]
Notation trunc := truncn (only parsing).
Notation floor := floor.
Notation ceil := ceil.
Notation nat_num := nat_num.
Notation int_num := int_num.
Notation archi_bound := bound.
End Def.
Module intArchimedean.
Section intArchimedean.
Implicit Types n : int.
Fact floor_subproof n :
if n \is real_num then n%:~R <= n < (n + 1)%:~R else n == 0.
Fact intrP n : reflect (exists m, n = m%:~R) true.
Fact natrP n : reflect (exists m, n = m%:R) (0 <= n).
Proof.
End intArchimedean.
End intArchimedean.
#[export]
HB.instance Definition _ :=
@NumDomain_hasFloorCeilTruncn.Build int id id _ xpredT nneg_num_pred
intArchimedean.floor_subproof (fun=> esym (opprK _)) (fun=> erefl)
intArchimedean.intrP intArchimedean.natrP.
Module Import Theory.
Export Num.Theory.
Section ArchiNumDomainTheory.
Variable R : archiNumDomainType.
Implicit Types x y z : R.
Local Notation truncn := (@truncn R).
Local Notation floor := (@floor R).
Local Notation ceil := (@ceil R).
Local Notation nat_num := (@Def.nat_num R).
Local Notation int_num := (@Def.int_num R).
Local Lemma floorP x :
if x \is real_num then (floor x)%:~R <= x < (floor x + 1)%:~R
else floor x == 0.
Proof.
Lemma floorNceil x : floor x = - ceil (- x).
Proof.
Lemma ceilNfloor x : ceil x = - floor (- x).
Proof.
Lemma truncEfloor x : truncn x = if floor x is Posz n then n else 0.
Proof.
Lemma natrP x : reflect (exists n, x = n%:R) (x \is a nat_num).
Proof.
Lemma intrP x : reflect (exists m, x = m%:~R) (x \is a int_num).
Proof.
Lemma intr_int m : m%:~R \is a int_num
Proof.
Proof.
Lemma rpred_int_num (S : subringClosed R) x : x \is a int_num -> x \in S.
Lemma rpred_nat_num (S : semiringClosed R) x : x \is a nat_num -> x \in S.
Lemma int_num0 : 0 \is a int_num
Proof.
Proof.
Proof.
Proof.
Fact int_num_subring : subring_closed int_num.
#[export]
HB.instance Definition _ := GRing.isSubringClosed.Build R int_num_subdef
int_num_subring.
Fact nat_num_semiring : semiring_closed nat_num.
#[export]
HB.instance Definition _ := GRing.isSemiringClosed.Build R nat_num_subdef
nat_num_semiring.
Lemma Rreal_nat : {subset nat_num <= real_num}.
Proof.
Lemma intr_nat : {subset nat_num <= int_num}.
Lemma Rreal_int : {subset int_num <= real_num}.
Proof.
Lemma intrE x : (x \is a int_num) = (x \is a nat_num) || (- x \is a nat_num).
Proof.
Lemma natr_int n : n%:R \is a int_num.
#[local] Hint Resolve natr_int : core.
Lemma intr_normK x : x \is a int_num -> `|x| ^+ 2 = x ^+ 2.
Proof.
Lemma natr_normK x : x \is a nat_num -> `|x| ^+ 2 = x ^+ 2.
Proof.
Lemma natr_norm_int x : x \is a int_num -> `|x| \is a nat_num.
Proof.
Lemma natr_ge0 x : x \is a nat_num -> 0 <= x.
Lemma natr_gt0 x : x \is a nat_num -> (0 < x) = (x != 0).
Proof.
Lemma natrEint x : (x \is a nat_num) = (x \is a int_num) && (0 <= x).
Proof.
Lemma intrEge0 x : 0 <= x -> (x \is a int_num) = (x \is a nat_num).
Lemma intrEsign x : x \is a int_num -> x = (-1) ^+ (x < 0)%R * `|x|.
Lemma norm_natr x : x \is a nat_num -> `|x| = x.
Lemma natr_exp_even x n : ~~ odd n -> x \is a int_num -> x ^+ n \is a nat_num.
Proof.
Lemma norm_intr_ge1 x : x \is a int_num -> x != 0 -> 1 <= `|x|.
Lemma sqr_intr_ge1 x : x \is a int_num -> x != 0 -> 1 <= x ^+ 2.
Proof.
Lemma intr_ler_sqr x : x \is a int_num -> x <= x ^+ 2.
Proof.
move=> Zx; have [-> | nz_x] := eqVneq x 0; first by rewrite expr0n.
apply: le_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Rreal_int.
by rewrite -intr_normK // ler_eXnr // norm_intr_ge1.
Qed.
apply: le_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Rreal_int.
by rewrite -intr_normK // ler_eXnr // norm_intr_ge1.
Qed.
Lemma real_floor_itv x :
x \is real_num -> (floor x)%:~R <= x < (floor x + 1)%:~R.
Lemma real_floor_le x : x \is real_num -> (floor x)%:~R <= x.
Proof.
Lemma real_floorD1_gt x : x \is real_num -> x < (floor x + 1)%:~R.
Proof.
Lemma floor_def x m : m%:~R <= x < (m + 1)%:~R -> floor x = m.
Proof.
Lemma real_floor_ge_int x n : x \is real_num -> (n <= floor x) = (n%:~R <= x).
Proof.
move=> /real_floor_itv /andP[lefx ltxf1]; apply/idP/idP => lenx.
by apply: le_trans lefx; rewrite ler_int.
by rewrite -ltzD1 -(ltr_int R); apply: le_lt_trans ltxf1.
Qed.
by apply: le_trans lefx; rewrite ler_int.
by rewrite -ltzD1 -(ltr_int R); apply: le_lt_trans ltxf1.
Qed.
Lemma real_floor_lt_int x n : x \is real_num -> (floor x < n) = (x < n%:~R).
Proof.
Lemma real_floor_eq x n : x \is real_num ->
(floor x == n) = (n%:~R <= x < (n + 1)%:~R).
Proof.
Lemma le_floor : {homo floor : x y / x <= y}.
Proof.
Lemma intrKfloor : cancel intr floor.
Lemma intrEfloor x : (x \is a int_num) = ((floor x)%:~R == x).
Proof.
Lemma floorK : {in int_num, cancel floor intr}.
Proof.
Lemma floor0 : floor 0 = 0
Proof.
Proof.
Lemma real_floorDzr : {in int_num & real_num, {morph floor : x y / x + y}}.
Proof.
move=> _ y /intrP[m ->] Ry; apply: floor_def.
by rewrite -addrA 2!rmorphD /= intrKfloor lerD2l ltrD2l real_floor_itv.
Qed.
by rewrite -addrA 2!rmorphD /= intrKfloor lerD2l ltrD2l real_floor_itv.
Qed.
Lemma real_floorDrz : {in real_num & int_num, {morph floor : x y / x + y}}.
Proof.
Lemma floorN : {in int_num, {morph floor : x / - x}}.
Proof.
Lemma floorM : {in int_num &, {morph floor : x y / x * y}}.
Proof.
Lemma floorX n : {in int_num, {morph floor : x / x ^+ n}}.
Proof.
Lemma real_floor_ge0 x : x \is real_num -> (0 <= floor x) = (0 <= x).
Proof.
Lemma floor_lt0 x : (floor x < 0) = (x < 0).
Proof.
Lemma real_floor_le0 x : x \is real_num -> (floor x <= 0) = (x < 1).
Proof.
Lemma floor_gt0 x : (floor x > 0) = (x >= 1).
Proof.
Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
Proof.
Lemma floorpK : {in polyOver int_num, cancel (map_poly floor) (map_poly intr)}.
Proof.
Lemma floorpP (p : {poly R}) :
p \is a polyOver int_num -> {q | p = map_poly intr q}.
Lemma real_ceil_itv x : x \is real_num -> (ceil x - 1)%:~R < x <= (ceil x)%:~R.
Proof.
Lemma real_ceilB1_lt x : x \is real_num -> (ceil x - 1)%:~R < x.
Proof.
Lemma real_ceil_ge x : x \is real_num -> x <= (ceil x)%:~R.
Proof.
Lemma ceil_def x m : (m - 1)%:~R < x <= m%:~R -> ceil x = m.
Proof.
Lemma real_ceil_le_int x n : x \is real_num -> (ceil x <= n) = (x <= n%:~R).
Proof.
Lemma real_ceil_gt_int x n : x \is real_num -> (n < ceil x) = (n%:~R < x).
Proof.
Lemma real_ceil_eq x n : x \is real_num ->
(ceil x == n) = ((n - 1)%:~R < x <= n%:~R).
Proof.
Lemma le_ceil : {homo ceil : x y / x <= y}.
Proof.
Lemma intrKceil : cancel intr ceil.
Proof.
Lemma intrEceil x : (x \is a int_num) = ((ceil x)%:~R == x).
Proof.
Lemma ceilK : {in int_num, cancel ceil intr}.
Lemma ceil0 : ceil 0 = 0
Proof.
Proof.
Lemma real_ceilDzr : {in int_num & real_num, {morph ceil : x y / x + y}}.
Proof.
move=> x y x_int y_real.
by rewrite ceilNfloor opprD real_floorDzr ?rpredN // opprD -!ceilNfloor.
Qed.
by rewrite ceilNfloor opprD real_floorDzr ?rpredN // opprD -!ceilNfloor.
Qed.
Lemma real_ceilDrz : {in real_num & int_num, {morph ceil : x y / x + y}}.
Proof.
Lemma ceilN : {in int_num, {morph ceil : x / - x}}.
Proof.
Lemma ceilM : {in int_num &, {morph ceil : x y / x * y}}.
Lemma ceilX n : {in int_num, {morph ceil : x / x ^+ n}}.
Lemma real_ceil_ge0 x : x \is real_num -> (0 <= ceil x) = (-1 < x).
Proof.
Lemma ceil_lt0 x : (ceil x < 0) = (x <= -1).
Proof.
Lemma real_ceil_le0 x : x \is real_num -> (ceil x <= 0) = (x <= 0).
Proof.
Lemma ceil_gt0 x : (ceil x > 0) = (x > 0).
Proof.
Lemma ceil_neq0 x : (ceil x != 0) = (x <= -1) || (x > 0).
Proof.
Lemma real_ceil_floor x : x \is real_num ->
ceil x = floor x + (x \isn't a int_num).
Proof.
case Ix: (x \is a int_num) => Rx /=.
by apply/eqP; rewrite addr0 ceilNfloor eqr_oppLR floorN.
apply/ceil_def; rewrite addrK; move: (real_floor_itv Rx).
by rewrite le_eqVlt -intrEfloor Ix /= => /andP[-> /ltW].
Qed.
by apply/eqP; rewrite addr0 ceilNfloor eqr_oppLR floorN.
apply/ceil_def; rewrite addrK; move: (real_floor_itv Rx).
by rewrite le_eqVlt -intrEfloor Ix /= => /andP[-> /ltW].
Qed.
Lemma truncn_floor x : truncn x = if 0 <= x then `|floor x|%N else 0%N.
Proof.
Local Lemma truncnP x :
if 0 <= x then (truncn x)%:R <= x < (truncn x).+1%:R else truncn x == 0%N.
Proof.
Lemma truncn_itv x : 0 <= x -> (truncn x)%:R <= x < (truncn x).+1%:R.
Proof.
Lemma truncn_le x : ((truncn x)%:R <= x) = (0 <= x).
Lemma real_truncnS_gt x : x \is real_num -> x < (truncn x).+1%:R.
Proof.
Lemma truncn_def x n : n%:R <= x < n.+1%:R -> truncn x = n.
Proof.
Lemma truncn_ge_nat x n : 0 <= x -> (n <= truncn x)%N = (n%:R <= x).
Proof.
move=> /truncn_itv /andP[letx ltxt1]; apply/idP/idP => lenx.
by apply: le_trans letx; rewrite ler_nat.
by rewrite -ltnS -(ltr_nat R); apply: le_lt_trans ltxt1.
Qed.
by apply: le_trans letx; rewrite ler_nat.
by rewrite -ltnS -(ltr_nat R); apply: le_lt_trans ltxt1.
Qed.
Lemma truncn_gt_nat x n : (n < truncn x)%N = (n.+1%:R <= x).
Proof.
Lemma truncn_lt_nat x n : 0 <= x -> (truncn x < n)%N = (x < n%:R).
Proof.
Lemma real_truncn_le_nat x n :
x \is real_num -> (truncn x <= n)%N = (x < n.+1%:R).
Proof.
Lemma truncn_eq x n : 0 <= x -> (truncn x == n) = (n%:R <= x < n.+1%:R).
Proof.
Lemma le_truncn : {homo truncn : x y / x <= y >-> (x <= y)%N}.
Proof.
Lemma natrK : cancel (GRing.natmul 1) truncn.
Proof.
Lemma natrEtruncn x : (x \is a nat_num) = ((truncn x)%:R == x).
Lemma archi_boundP x : 0 <= x -> x < (bound x)%:R.
Proof.
move=> x_ge0; case/truncn_itv/andP: (normr_ge0 x) => _.
exact/le_lt_trans/real_ler_norm/ger0_real.
Qed.
exact/le_lt_trans/real_ler_norm/ger0_real.
Qed.
Lemma truncnK : {in nat_num, cancel truncn (GRing.natmul 1)}.
Proof.
Lemma truncn0 : truncn 0 = 0%N
Proof.
Proof.
Lemma truncnD :
{in nat_num & nneg_num, {morph truncn : x y / x + y >-> (x + y)%N}}.
Proof.
move=> _ y /natrP[n ->] y_ge0; apply: truncn_def.
by rewrite -addnS !natrD !natrK lerD2l ltrD2l truncn_itv.
Qed.
by rewrite -addnS !natrD !natrK lerD2l ltrD2l truncn_itv.
Qed.
Lemma truncnM : {in nat_num &, {morph truncn : x y / x * y >-> (x * y)%N}}.
Lemma truncnX n : {in nat_num, {morph truncn : x / x ^+ n >-> (x ^ n)%N}}.
Lemma truncn_gt0 x : (0 < truncn x)%N = (1 <= x).
Proof.
Lemma truncn0Pn x : reflect (truncn x = 0%N) (~~ (1 <= x)).
Proof.
Lemma sum_truncnK I r (P : pred I) F : (forall i, P i -> F i \is a nat_num) ->
(\sum_(i <- r | P i) truncn (F i))%:R = \sum_(i <- r | P i) F i.
Lemma prod_truncnK I r (P : pred I) F : (forall i, P i -> F i \is a nat_num) ->
(\prod_(i <- r | P i) truncn (F i))%:R = \prod_(i <- r | P i) F i.
Lemma natr_sum_eq1 (I : finType) (P : pred I) (F : I -> R) :
(forall i, P i -> F i \is a nat_num) -> \sum_(i | P i) F i = 1 ->
{i : I | [/\ P i, F i = 1 & forall j, j != i -> P j -> F j = 0]}.
Proof.
move=> natF /eqP; rewrite -sum_truncnK// -[1]/1%:R eqr_nat => /sum_nat_eq1 exi.
have [i /and3P[Pi /eqP f1 /forallP a]] : {i : I | [&& P i, truncn (F i) == 1
& [forall j : I, ((j != i) ==> P j ==> (truncn (F j) == 0))]]}.
apply/sigW; have [i [Pi /eqP f1 a]] := exi; exists i; apply/and3P; split=> //.
by apply/forallP => j; apply/implyP => ji; apply/implyP => Pj; apply/eqP/a.
exists i; split=> [//||j ji Pj]; rewrite -[LHS]truncnK ?natF ?f1//; apply/eqP.
by rewrite -[0]/0%:R eqr_nat; apply: implyP Pj; apply: implyP ji; apply: a.
Qed.
have [i /and3P[Pi /eqP f1 /forallP a]] : {i : I | [&& P i, truncn (F i) == 1
& [forall j : I, ((j != i) ==> P j ==> (truncn (F j) == 0))]]}.
apply/sigW; have [i [Pi /eqP f1 a]] := exi; exists i; apply/and3P; split=> //.
by apply/forallP => j; apply/implyP => ji; apply/implyP => Pj; apply/eqP/a.
exists i; split=> [//||j ji Pj]; rewrite -[LHS]truncnK ?natF ?f1//; apply/eqP.
by rewrite -[0]/0%:R eqr_nat; apply: implyP Pj; apply: implyP ji; apply: a.
Qed.
Lemma natr_mul_eq1 x y :
x \is a nat_num -> y \is a nat_num -> (x * y == 1) = (x == 1) && (y == 1).
Lemma natr_prod_eq1 (I : finType) (P : pred I) (F : I -> R) :
(forall i, P i -> F i \is a nat_num) -> \prod_(i | P i) F i = 1 ->
forall i, P i -> F i = 1.
Proof.
move=> natF /eqP; rewrite -prod_truncnK// -[1]/1%:R eqr_nat prod_nat_seq_eq1.
move/allP => a i Pi; apply/eqP; rewrite -[F i]truncnK ?natF// eqr_nat.
by apply: implyP Pi; apply: a; apply: mem_index_enum.
Qed.
move/allP => a i Pi; apply/eqP; rewrite -[F i]truncnK ?natF// eqr_nat.
by apply: implyP Pi; apply: a; apply: mem_index_enum.
Qed.
Variables (U V : lmodType R) (f : {additive U -> V}).
Lemma raddfZ_nat a u : a \is a nat_num -> f (a *: u) = a *: f u.
Lemma rpredZ_nat (S : addrClosed V) :
{in nat_num & S, forall z u, z *: u \in S}.
Lemma raddfZ_int a u : a \is a int_num -> f (a *: u) = a *: f u.
Proof.
Lemma rpredZ_int (S : zmodClosed V) :
{in int_num & S, forall z u, z *: u \in S}.
Proof.
Implicit Type nu : {rmorphism R -> R}.
Lemma aut_natr nu : {in nat_num, nu =1 id}.
Proof.
Lemma aut_intr nu : {in int_num, nu =1 id}.
Proof.
End ArchiNumDomainTheory.
#[deprecated(since="mathcomp 2.4.0", use=truncn_itv)]
Notation trunc_itv := truncn_itv (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn_def)]
Notation trunc_def := truncn_def (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncnK)]
Notation truncK := truncnK (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn0)]
Notation trunc0 := truncn0 (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn1)]
Notation trunc1 := truncn1 (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncnD)]
Notation truncD := truncnD (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncnM)]
Notation truncM := truncnM (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncnX)]
Notation truncX := truncnX (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn_gt0)]
Notation trunc_gt0 := truncn_gt0 (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn0Pn)]
Notation trunc0Pn := truncn0Pn (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=sum_truncnK)]
Notation sum_truncK := sum_truncnK (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=prod_truncnK)]
Notation prod_truncK := prod_truncnK (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=truncn_floor)]
Notation trunc_floor := truncn_floor (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=real_floor_le)]
Notation real_ge_floor := real_floor_le (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=real_floorD1_gt)]
Notation real_lt_succ_floor := real_floorD1_gt (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=real_ceilB1_lt)]
Notation real_gt_pred_ceil := real_floorD1_gt (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=real_ceil_ge)]
Notation real_le_ceil := real_ceil_ge (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=le_ceil)]
Notation ceil_le := le_ceil (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=natrEtruncn)]
Notation natrE := natrEtruncn (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=le_ceil)]
Notation le_ceil_tmp := le_ceil (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=real_floor_ge_int)]
Notation real_floor_ge_int_tmp := real_floor_ge_int (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=real_ceil_le_int)]
Notation real_ceil_le_int_tmp := real_ceil_le_int (only parsing).
Arguments natrK {R} _%_N.
Arguments intrKfloor {R}.
Arguments intrKceil {R}.
Arguments natrP {R x}.
Arguments intrP {R x}.
#[global] Hint Resolve truncn0 truncn1 : core.
#[global] Hint Resolve floor0 floor1 : core.
#[global] Hint Resolve ceil0 ceil1 : core.
#[global] Hint Extern 0 (is_true (_%:R \is a nat_num)) => apply: natr_nat : core.
#[global] Hint Extern 0 (is_true (_%:R \in nat_num_subdef)) => apply: natr_nat : core.
#[global] Hint Extern 0 (is_true (_%:~R \is a int_num)) => apply: intr_int : core.
#[global] Hint Extern 0 (is_true (_%:~R \in int_num_subdef)) => apply: intr_int : core.
#[global] Hint Extern 0 (is_true (_%:R \is a int_num)) => apply: natr_int : core.
#[global] Hint Extern 0 (is_true (_%:R \in int_num_subdef)) => apply: natr_int : core.
#[global] Hint Extern 0 (is_true (0 \is a nat_num)) => apply: nat_num0 : core.
#[global] Hint Extern 0 (is_true (0 \in nat_num_subdef)) => apply: nat_num0 : core.
#[global] Hint Extern 0 (is_true (1 \is a nat_num)) => apply: nat_num1 : core.
#[global] Hint Extern 0 (is_true (1 \in int_num_subdef)) => apply: nat_num1 : core.
#[global] Hint Extern 0 (is_true (0 \is a int_num)) => apply: int_num0 : core.
#[global] Hint Extern 0 (is_true (0 \in int_num_subdef)) => apply: int_num0 : core.
#[global] Hint Extern 0 (is_true (1 \is a int_num)) => apply: int_num1 : core.
#[global] Hint Extern 0 (is_true (1 \in int_num_subdef)) => apply: int_num1 : core.
Section ArchiRealDomainTheory.
Variables (R : archiRealDomainType).
Implicit Type x : R.
Lemma upper_nthrootP x i : (bound x <= i)%N -> x < 2%:R ^+ i.
Proof.
case/truncn_itv/andP: (normr_ge0 x) => _ /ltr_normlW xlt le_b_i.
by rewrite (lt_le_trans xlt) // -natrX ler_nat (ltn_trans le_b_i) // ltn_expl.
Qed.
by rewrite (lt_le_trans xlt) // -natrX ler_nat (ltn_trans le_b_i) // ltn_expl.
Qed.
Lemma truncnS_gt x : x < (truncn x).+1%:R.
Proof.
Lemma truncn_le_nat x n : (truncn x <= n)%N = (x < n.+1%:R).
Proof.
Lemma floor_itv x : (floor x)%:~R <= x < (floor x + 1)%:~R.
Proof.
Lemma floor_le x : (floor x)%:~R <= x
Proof.
Lemma floorD1_gt x : x < (floor x + 1)%:~R.
Proof.
Lemma floor_ge_int x n : (n <= floor x) = (n%:~R <= x).
Proof.
Lemma floor_lt_int x n : (floor x < n) = (x < n%:~R).
Proof.
Lemma floor_eq x n : (floor x == n) = (n%:~R <= x < (n + 1)%:~R).
Proof.
Lemma floorDzr : {in @int_num R, {morph floor : x y / x + y}}.
Proof.
Lemma floorDrz x y : y \is a int_num -> floor (x + y) = floor x + floor y.
Proof.
Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).
Proof.
Lemma floor_le0 x : (floor x <= 0) = (x < 1).
Proof.
Lemma ceil_itv x : (ceil x - 1)%:~R < x <= (ceil x)%:~R.
Proof.
Lemma ceilB1_lt x : (ceil x - 1)%:~R < x.
Proof.
Lemma ceil_ge x : x <= (ceil x)%:~R
Proof.
Lemma ceil_le_int x n : (ceil x <= n) = (x <= n%:~R).
Proof.
Lemma ceil_gt_int x n : (n < ceil x) = (n%:~R < x).
Proof.
Lemma ceil_eq x n : (ceil x == n) = ((n - 1)%:~R < x <= n%:~R).
Proof.
Lemma ceilDzr : {in @int_num R, {morph ceil : x y / x + y}}.
Proof.
Lemma ceilDrz x y : y \is a int_num -> ceil (x + y) = ceil x + ceil y.
Proof.
Lemma ceil_ge0 x : (0 <= ceil x) = (-1 < x).
Proof.
Lemma ceil_le0 x : (ceil x <= 0) = (x <= 0).
Proof.
Lemma ceil_floor x : ceil x = floor x + (x \isn't a int_num).
Proof.
End ArchiRealDomainTheory.
#[deprecated(since="mathcomp 2.4.0", use=floor_le)]
Notation ge_floor := floor_le (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=floorD1_gt)]
Notation lt_succ_floor := floorD1_gt (only parsing).
#[deprecated(since="mathcomp 2.4.0", use=ceilB1_lt)]
Notation gt_pred_ceil := ceilB1_lt (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=floor_le)]
Notation floor_le_tmp := floor_le (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=floor_ge_int)]
Notation floor_ge_int_tmp := floor_ge_int (only parsing).
#[deprecated(since="mathcomp 2.5.0", use=ceil_le_int)]
Notation ceil_le_int_tmp := ceil_le_int (only parsing).
Section ArchiNumFieldTheory.
Variables (R : archiNumFieldType) (nu : {rmorphism R -> R}).
Lemma natr_aut x : (nu x \is a nat_num) = (x \is a nat_num).
Lemma intr_aut x : (nu x \is a int_num) = (x \is a int_num).
End ArchiNumFieldTheory.
Section ArchiClosedFieldTheory.
Variable R : archiClosedFieldType.
Implicit Type x : R.
Lemma conj_natr x : x \is a nat_num -> x^* = x.
Lemma conj_intr x : x \is a int_num -> x^* = x.
End ArchiClosedFieldTheory.
Section ZnatPred.
Lemma Znat_def (n : int) : (n \is a nat_num) = (0 <= n).
Proof.
by []. Qed.
Lemma ZnatP (m : int) : reflect (exists n : nat, m = n) (m \is a nat_num).
Proof.
by case: m => m; constructor; [exists m | case]. Qed.
End ZnatPred.
End Theory.
HB.factory Record NumDomain_hasTruncn R & Num.NumDomain R := {
truncn : R -> nat;
nat_num : pred R;
int_num : pred R;
truncn_subproof : forall x,
if 0 <= x then (truncn x)%:R <= x < (truncn x).+1%:R else truncn x == 0;
natrE : forall x, nat_num x = ((truncn x)%:R == x);
intrE : forall x, int_num x = nat_num x || nat_num (- x);
}.
#[deprecated(since="mathcomp 2.4.0", use=NumDomain_hasTruncn)]
Notation NumDomain_isArchimedean R := (NumDomain_hasTruncn R) (only parsing).
Module NumDomain_isArchimedean.
#[deprecated(since="mathcomp 2.4.0", use=NumDomain_hasTruncn.Build)]
Notation Build T U := (NumDomain_hasTruncn.Build T U) (only parsing).
End NumDomain_isArchimedean.
HB.builders Context R & NumDomain_hasTruncn R.
Fact truncn_itv x : 0 <= x -> (truncn x)%:R <= x < (truncn x).+1%:R.
Proof.
Definition floor (x : R) : int :=
if 0 <= x then Posz (truncn x)
else if x < 0 then - Posz (truncn (- x) + ~~ int_num x) else 0.
Fact floor_subproof x :
if x \is real_num then (floor x)%:~R <= x < (floor x + 1)%:~R else floor x == 0.
Proof.
rewrite /floor intrE !natrE negb_or realE.
case: (comparableP x 0) (@truncn_itv x) => //=;
try by rewrite -PoszD addn1 -pmulrn => _ ->.
move=> x_lt0 _; move: (truncn_subproof x); rewrite lt_geF // => /eqP ->.
rewrite gt_eqF //=; move: x_lt0.
rewrite [_ + 1]addrC -opprB !intrN lerNl ltrNr andbC -oppr_gt0.
move: {x}(- x) => x x_gt0; rewrite PoszD -addrA -PoszD.
have ->: Posz ((truncn x)%:R != x) - 1 = - Posz ((truncn x)%:R == x).
by case: eqP.
have := truncn_itv (ltW x_gt0); rewrite le_eqVlt.
case: eqVneq => /=; last first.
by rewrite subr0 addn1 -!pmulrn => _ /andP[-> /ltW ->].
by rewrite intrB mulr1z addn0 -!pmulrn => -> _; rewrite gtrBl lexx andbT.
Qed.
case: (comparableP x 0) (@truncn_itv x) => //=;
try by rewrite -PoszD addn1 -pmulrn => _ ->.
move=> x_lt0 _; move: (truncn_subproof x); rewrite lt_geF // => /eqP ->.
rewrite gt_eqF //=; move: x_lt0.
rewrite [_ + 1]addrC -opprB !intrN lerNl ltrNr andbC -oppr_gt0.
move: {x}(- x) => x x_gt0; rewrite PoszD -addrA -PoszD.
have ->: Posz ((truncn x)%:R != x) - 1 = - Posz ((truncn x)%:R == x).
by case: eqP.
have := truncn_itv (ltW x_gt0); rewrite le_eqVlt.
case: eqVneq => /=; last first.
by rewrite subr0 addn1 -!pmulrn => _ /andP[-> /ltW ->].
by rewrite intrB mulr1z addn0 -!pmulrn => -> _; rewrite gtrBl lexx andbT.
Qed.
Fact truncnE x : truncn x = if floor x is Posz n then n else 0.
Proof.
rewrite /floor.
case: (comparableP x 0) (truncn_subproof x) => [+ /eqP ->| |_ /eqP ->|] //=.
by case: (_ + _)%N.
Qed.
case: (comparableP x 0) (truncn_subproof x) => [+ /eqP ->| |_ /eqP ->|] //=.
by case: (_ + _)%N.
Qed.
Fact truncn_def x n : n%:R <= x < n.+1%:R -> truncn x = n.
Proof.
Fact natrK : cancel (GRing.natmul 1) truncn.
Proof.
Fact intrP x : reflect (exists n, x = n%:~R) (int_num x).
Proof.
Fact natrP x : reflect (exists n, x = n%:R) (nat_num x).
Proof.
HB.instance Definition _ :=
@NumDomain_hasFloorCeilTruncn.Build R floor _ truncn int_num nat_num
floor_subproof (fun=> erefl) truncnE intrP natrP.
HB.end.
HB.factory Record NumDomain_bounded_isArchimedean R & Num.NumDomain R := {
archi_bound_subproof : Num.archimedean_axiom R
}.
HB.builders Context R & NumDomain_bounded_isArchimedean R.
Implicit Type x : R.
Definition bound x := sval (sigW (archi_bound_subproof x)).
Fact boundP x : 0 <= x -> x < (bound x)%:R.
Fact truncn_sig x : {m | 0 <= x -> m%:R <= x < m.+1%:R}.
Proof.
have [Rx | _] := boolP (0 <= x); last by exists 0%N.
have/ex_minnP[n lt_x_n1 min_n]: exists n, x < n.+1%:R.
by exists (bound x); rewrite (lt_trans (boundP Rx)) ?ltr_nat.
exists n => _; rewrite {}lt_x_n1 andbT; case: n min_n => //= n min_n.
rewrite real_leNgt ?rpred_nat ?ger0_real //; apply/negP => /min_n.
by rewrite ltnn.
Qed.
have/ex_minnP[n lt_x_n1 min_n]: exists n, x < n.+1%:R.
by exists (bound x); rewrite (lt_trans (boundP Rx)) ?ltr_nat.
exists n => _; rewrite {}lt_x_n1 andbT; case: n min_n => //= n min_n.
rewrite real_leNgt ?rpred_nat ?ger0_real //; apply/negP => /min_n.
by rewrite ltnn.
Qed.
Definition truncn x := if 0 <= x then sval (truncn_sig x) else 0%N.
Fact truncn_subproof x :
if 0 <= x then (truncn x)%:R <= x < (truncn x).+1%:R else truncn x == 0%N.
Proof.
rewrite /truncn; case: truncn_sig => // n hn.
by case: ifP => x_ge0; rewrite ?(ifT _ _ x_ge0) ?(ifF _ _ x_ge0) // hn.
Qed.
by case: ifP => x_ge0; rewrite ?(ifT _ _ x_ge0) ?(ifF _ _ x_ge0) // hn.
Qed.
HB.instance Definition _ := NumDomain_hasTruncn.Build R
truncn_subproof (fun => erefl) (fun => erefl).
HB.end.
Module Exports. HB.reexport. End Exports.
Notation nat := nat_num.
Notation int := int_num.
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealDomain)]
Notation ArchiDomain T := (ArchiRealDomain T) (only parsing).
Module ArchiDomain.
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealDomain.type)]
Notation type := ArchiRealDomain.type (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealDomain.copy)]
Notation copy T C := (ArchiRealDomain.copy T C) (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealDomain.on)]
Notation on T := (ArchiRealDomain.on T) (only parsing).
End ArchiDomain.
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealField)]
Notation ArchiField T := (ArchiRealField T) (only parsing).
Module ArchiField.
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealField.type)]
Notation type := ArchiRealField.type (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealField.copy)]
Notation copy T C := (ArchiRealField.copy T C) (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=Num.ArchiRealField.on)]
Notation on T := (ArchiRealField.on T) (only parsing).
End ArchiField.
#[deprecated(since="mathcomp 2.3.0", use=real_floorDzr)]
Notation floorD := real_floorDzr (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=real_ceilDzr)]
Notation ceilD := real_ceilDzr (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=real_ceilDzr)]
Notation real_ceilD := real_ceilDzr (only parsing).
End Num.
Export Num.Exports.
#[deprecated(since="mathcomp 2.3.0", use=archiRealDomainType)]
Notation archiDomainType := archiRealDomainType (only parsing).
#[deprecated(since="mathcomp 2.3.0", use=archiRealFieldType)]
Notation archiFieldType := archiRealFieldType (only parsing).