Library mathcomp.algebra.archimedean

(* (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 fintype bigop order ssralg poly ssrnum 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.

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

Module Num.
Import Num.Def.


#[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.

#[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.

#[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.

#[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.

#[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.

#[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.

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", note="Renamed to truncn.")]
Notation trunc := truncn.

Module Def.
Export ssrnum.Num.Def.

Notation truncn := truncn.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn.")]
Notation trunc := truncn.
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.

Lemma floorP n : if n \is Rreal then n%:~R ≤ n < (n + 1)%:~R else n == 0.

Lemma intrP n : reflect (∃ m, n = m%:~R) true.

Lemma natrP n : reflect (∃ m, n = m%:R) (0 ≤ n).

End intArchimedean.
End intArchimedean.

#[export]
HB.instance Definition _ :=
  @NumDomain_hasFloorCeilTruncn.Build int id id _ xpredT Rnneg_pred
    intArchimedean.floorP (fun⇒ esym (opprK _)) (fun⇒ erefl)
    intArchimedean.intrP intArchimedean.natrP.

Module Import Theory.
Export ssrnum.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 Rreal then (floor x)%:~R ≤ x < (floor x + 1)%:~R else floor x == 0.

Lemma floorNceil x : floor x = - ceil (- x).

Lemma ceilNfloor x : ceil x = - floor (- x).

Lemma truncEfloor x : truncn x = if floor x is Posz n then n else 0.

Lemma natrP x : reflect (∃ n, x = n%:R) (x \is a nat_num).

Lemma intrP x : reflect (∃ m, x = m%:~R) (x \is a int_num).

int_num and nat_num

Lemma intr_int m : m%:~R \is a int_num.
Lemma natr_nat n : n%:R \is a nat_num.
#[local] Hint Resolve intr_int natr_nat : core.

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.
Lemma int_num1 : 1 \is a int_num.
Lemma nat_num0 : 0 \is a nat_num.
Lemma nat_num1 : 1 \is a nat_num.
#[local] Hint Resolve int_num0 int_num1 nat_num0 nat_num1 : core.

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 ≤ Rreal}.

Lemma intr_nat : {subset nat_num ≤ int_num}.

Lemma Rreal_int : {subset int_num ≤ Rreal}.

Lemma intrE x : (x \is a int_num) = (x \is a nat_num) || (- x \is a nat_num).

Lemma intr_normK x : x \is a int_num → `|x| ^+ 2 = x ^+ 2.

Lemma natr_normK x : x \is a nat_num → `|x| ^+ 2 = x ^+ 2.

Lemma natr_norm_int x : x \is a int_num → `|x| \is a nat_num.

Lemma natr_ge0 x : x \is a nat_num → 0 ≤ x.

Lemma natr_gt0 x : x \is a nat_num → (0 < x) = (x != 0).

Lemma natrEint x : (x \is a nat_num) = (x \is a int_num) && (0 ≤ x).

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.

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.

Lemma intr_ler_sqr x : x \is a int_num → x ≤ x ^+ 2.

floor and int_num

Lemma real_floor_itv x : x \is Rreal → (floor x)%:~R ≤ x < (floor x + 1)%:~R.

Lemma real_floor_le x : x \is Rreal → (floor x)%:~R ≤ x.

Lemma real_floorD1_gt x : x \is Rreal → x < (floor x + 1)%:~R.

Lemma floor_def x m : m%:~R ≤ x < (m + 1)%:~R → floor x = m.

TODO: rename to real_floor_ge_int, once the currently deprecated one has been removed
Lemma real_floor_ge_int_tmp x n : x \is Rreal → (n ≤ floor x) = (n%:~R ≤ x).

#[deprecated(since="mathcomp 2.4.0", note="Use real_floor_ge_int_tmp instead.")]
Lemma real_floor_ge_int x n : x \is Rreal → (n%:~R ≤ x) = (n ≤ floor x).

Lemma real_floor_lt_int x n : x \is Rreal → (floor x < n) = (x < n%:~R).

Lemma real_floor_eq x n : x \is Rreal →
  (floor x == n) = (n%:~R ≤ x < (n + 1)%:~R).

Lemma le_floor : {homo floor : x y / x ≤ y}.

Lemma intrKfloor : cancel intr floor.

Lemma natr_int n : n%:R \is a int_num.
#[local] Hint Resolve natr_int : core.

Lemma intrEfloor x : x \is a int_num = ((floor x)%:~R == x).

Lemma floorK : {in int_num, cancel floor intr}.

Lemma floor0 : floor 0 = 0.
Lemma floor1 : floor 1 = 1.
#[local] Hint Resolve floor0 floor1 : core.

Lemma real_floorDzr : {in int_num & Rreal, {morph floor : x y / x + y}}.

Lemma real_floorDrz : {in Rreal & int_num, {morph floor : x y / x + y}}.

Lemma floorN : {in int_num, {morph floor : x / - x}}.

Lemma floorM : {in int_num &, {morph floor : x y / x × y}}.

Lemma floorX n : {in int_num, {morph floor : x / x ^+ n}}.

Lemma real_floor_ge0 x : x \is Rreal → (0 ≤ floor x) = (0 ≤ x).

Lemma floor_lt0 x : (floor x < 0) = (x < 0).

Lemma real_floor_le0 x : x \is Rreal → (floor x ≤ 0) = (x < 1).

Lemma floor_gt0 x : (floor x > 0) = (x ≥ 1).

Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x ≥ 1).

Lemma floorpK : {in polyOver int_num, cancel (map_poly floor) (map_poly intr)}.

Lemma floorpP (p : {poly R}) :
  p \is a polyOver int_num → {q | p = map_poly intr q}.

ceil and int_num

Lemma real_ceil_itv x : x \is Rreal → (ceil x - 1)%:~R < x ≤ (ceil x)%:~R.

Lemma real_ceilB1_lt x : x \is Rreal → (ceil x - 1)%:~R < x.

Lemma real_ceil_ge x : x \is Rreal → x ≤ (ceil x)%:~R.

Lemma ceil_def x m : (m - 1)%:~R < x ≤ m%:~R → ceil x = m.

TODO: rename to real_ceil_le_int, once the currently deprecated one has been removed
Lemma real_ceil_le_int_tmp x n : x \is Rreal → (ceil x ≤ n) = (x ≤ n%:~R).

#[deprecated(since="mathcomp 2.4.0", note="Use real_ceil_le_int_tmp instead.")]
Lemma real_ceil_le_int x n : x \is Rreal → x ≤ n%:~R = (ceil x ≤ n).

Lemma real_ceil_gt_int x n : x \is Rreal → (n < ceil x) = (n%:~R < x).

Lemma real_ceil_eq x n : x \is Rreal →
  (ceil x == n) = ((n - 1)%:~R < x ≤ n%:~R).

TODO: rename to le_ceil, once the currently deprecated one has been removed
Lemma le_ceil_tmp : {homo ceil : x y / x ≤ y}.

Lemma intrKceil : cancel intr ceil.

Lemma intrEceil x : x \is a int_num = ((ceil x)%:~R == x).

Lemma ceilK : {in int_num, cancel ceil intr}.

Lemma ceil0 : ceil 0 = 0.
Lemma ceil1 : ceil 1 = 1.
#[local] Hint Resolve ceil0 ceil1 : core.

Lemma real_ceilDzr : {in int_num & Rreal, {morph ceil : x y / x + y}}.

Lemma real_ceilDrz : {in Rreal & int_num, {morph ceil : x y / x + y}}.

Lemma ceilN : {in int_num, {morph ceil : x / - x}}.

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 Rreal → (0 ≤ ceil x) = (-1 < x).

Lemma ceil_lt0 x : (ceil x < 0) = (x ≤ -1).

Lemma real_ceil_le0 x : x \is Rreal → (ceil x ≤ 0) = (x ≤ 0).

Lemma ceil_gt0 x : (ceil x > 0) = (x > 0).

Lemma ceil_neq0 x : (ceil x != 0) = (x ≤ -1) || (x > 0).

Lemma real_ceil_floor x : x \is Rreal →
  ceil x = floor x + (x \isn't a int_num).

Relating Cnat and oldCnat.

Lemma truncn_floor x : truncn x = if 0 ≤ x then `|floor x|%N else 0%N.

trunc and nat_num

Local Lemma truncnP x :
  if 0 ≤ x then (truncn x)%:R ≤ x < (truncn x).+1%:R else truncn x == 0%N.

Lemma truncn_itv x : 0 ≤ x → (truncn x)%:R ≤ x < (truncn x).+1%:R.

Lemma truncn_le x : (truncn x)%:R ≤ x = (0 ≤ x).

Lemma real_truncnS_gt x : x \is Rreal → x < (truncn x).+1%:R.

Lemma truncn_def x n : n%:R ≤ x < n.+1%:R → truncn x = n.

Lemma truncn_ge_nat x n : 0 ≤ x → (n ≤ truncn x)%N = (n%:R ≤ x).

Lemma truncn_gt_nat x n : (n < truncn x)%N = (n.+1%:R ≤ x).

Lemma truncn_lt_nat x n : 0 ≤ x → (truncn x < n)%N = (x < n%:R).

Lemma real_truncn_le_nat x n : x \is Rreal → (truncn x ≤ n)%N = (x < n.+1%:R).

Lemma truncn_eq x n : 0 ≤ x → (truncn x == n) = (n%:R ≤ x < n.+1%:R).

Lemma le_truncn : {homo truncn : x y / x ≤ y >-> (x ≤ y)%N}.

Lemma natrK : cancel (GRing.natmul 1) truncn.

Lemma natrEtruncn x : (x \is a nat_num) = ((truncn x)%:R == x).

Lemma archi_boundP x : 0 ≤ x → x < (bound x)%:R.

Lemma truncnK : {in nat_num, cancel truncn (GRing.natmul 1)}.

Lemma truncn0 : truncn 0 = 0%N.
Lemma truncn1 : truncn 1 = 1%N.
#[local] Hint Resolve truncn0 truncn1 : core.

Lemma truncnD :
  {in nat_num & Rnneg, {morph truncn : x y / x + y >-> (x + y)%N}}.

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).

Lemma truncn0Pn x : reflect (truncn x = 0%N) (~~ (1 ≤ x)).

Lemma sum_truncnK I r (P : pred I) F : (∀ 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 : (∀ 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) :
     (∀ i, P i → F i \is a nat_num) → \sum_(i | P i) F i = 1 →
   {i : I | [/\ P i, F i = 1 & ∀ j, j != i → P j → F j = 0]}.

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) :
    (∀ i, P i → F i \is a nat_num) → \prod_(i | P i) F i = 1 →
  ∀ i, P i → F i = 1.

predCmod
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, ∀ z u, z *: u \in S}.

Lemma raddfZ_int a u : a \is a int_num → f (a *: u) = a *: f u.

Lemma rpredZ_int (S : zmodClosed V) :
  {in int_num & S, ∀ z u, z *: u \in S}.

autC
Implicit Type nu : {rmorphism R → R}.

Lemma aut_natr nu : {in nat_num, nu =1 id}.

Lemma aut_intr nu : {in int_num, nu =1 id}.

End ArchiNumDomainTheory.

#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn_itv.")]
Notation trunc_itv := truncn_itv.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn_def.")]
Notation trunc_def := truncn_def.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncnK.")]
Notation truncK := truncnK.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn0.")]
Notation trunc0 := truncn0.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn1.")]
Notation trunc1 := truncn1.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncnD.")]
Notation truncD := truncnD.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncnM.")]
Notation truncM := truncnM.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncnX.")]
Notation truncX := truncnX.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn_gt0.")]
Notation trunc_gt0 := truncn_gt0.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn0Pn.")]
Notation trunc0Pn := truncn0Pn.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to sum_truncnK.")]
Notation sum_truncK := sum_truncnK.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to prod_truncnK.")]
Notation prod_truncK := prod_truncnK.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to truncn_floor.")]
Notation trunc_floor := truncn_floor.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to real_floor_le.")]
Notation real_ge_floor := real_floor_le.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to real_floorD1_gt.")]
Notation real_lt_succ_floor := real_floorD1_gt.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to real_ceilB1_lt.")]
Notation real_gt_pred_ceil := real_floorD1_gt.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to real_ceil_ge.")]
Notation real_le_ceil := real_ceil_ge.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to le_floor.")]
Notation floor_le := le_floor.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to le_ceil.")]
Notation ceil_le := le_ceil_tmp.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to natrEtruncn.")]
Notation natrE := natrEtruncn.

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.

Lemma truncnS_gt x : x < (truncn x).+1%:R.

Lemma truncn_le_nat x n : (truncn x ≤ n)%N = (x < n.+1%:R).

Lemma floor_itv x : (floor x)%:~R ≤ x < (floor x + 1)%:~R.

TODO: rename to floor_le, once the deprecated one has been removed
Lemma floor_le_tmp x : (floor x)%:~R ≤ x.

Lemma floorD1_gt x : x < (floor x + 1)%:~R.

#[deprecated(since="mathcomp 2.4.0", note="Use floor_ge_int_tmp instead.")]
Lemma floor_ge_int x n : n%:~R ≤ x = (n ≤ floor x).

TODO: rename to floor_ge_int, once the currently deprecated one has been removed
Lemma floor_ge_int_tmp x n : (n ≤ floor x) = (n%:~R ≤ x).

Lemma floor_lt_int x n : (floor x < n) = (x < n%:~R).

Lemma floor_eq x n : (floor x == n) = (n%:~R ≤ x < (n + 1)%:~R).

Lemma floorDzr : {in @int_num R, {morph floor : x y / x + y}}.

Lemma floorDrz x y : y \is a int_num → floor (x + y) = floor x + floor y.

Lemma floor_ge0 x : (0 ≤ floor x) = (0 ≤ x).

Lemma floor_le0 x : (floor x ≤ 0) = (x < 1).

Lemma ceil_itv x : (ceil x - 1)%:~R < x ≤ (ceil x)%:~R.

Lemma ceilB1_lt x : (ceil x - 1)%:~R < x.

Lemma ceil_ge x : x ≤ (ceil x)%:~R.

#[deprecated(since="mathcomp 2.4.0", note="Use ceil_le_int_tmp instead.")]
Lemma ceil_le_int x n : x ≤ n%:~R = (ceil x ≤ n).

TODO: rename to ceil_le_int, once the currently deprecated one has been removed
Lemma ceil_le_int_tmp x n : (ceil x ≤ n) = (x ≤ n%:~R).

Lemma ceil_gt_int x n : (n < ceil x) = (n%:~R < x).

Lemma ceil_eq x n : (ceil x == n) = ((n - 1)%:~R < x ≤ n%:~R).

Lemma ceilDzr : {in @int_num R, {morph ceil : x y / x + y}}.

Lemma ceilDrz x y : y \is a int_num → ceil (x + y) = ceil x + ceil y.

Lemma ceil_ge0 x : (0 ≤ ceil x) = (-1 < x).

Lemma ceil_le0 x : (ceil x ≤ 0) = (x ≤ 0).

Lemma ceil_floor x : ceil x = floor x + (x \isn't a int_num).

End ArchiRealDomainTheory.

#[deprecated(since="mathcomp 2.4.0", note="Renamed to floor_le_tmp.")]
Notation ge_floor := floor_le_tmp.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to floorD1_gt.")]
Notation lt_succ_floor := floorD1_gt.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to ceilB1_lt.")]
Notation gt_pred_ceil := ceilB1_lt.
#[deprecated(since="mathcomp 2.4.0", note="Renamed to ceil_ge.")]
Notation le_ceil := ceil_ge.

Section ArchiNumFieldTheory.

autLmodC
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).

Lemma ZnatP (m : int) : reflect (∃ n : nat, m = n) (m \is a nat_num).

End ZnatPred.

End Theory.

Factories


#[deprecated(since="mathcomp 2.4.0",
             note="Use NumDomain_hasTruncn instead.")]
Notation NumDomain_isArchimedean R := (NumDomain_hasTruncn R) (only parsing).

Module NumDomain_isArchimedean.
#[deprecated(since="mathcomp 2.4.0",
             note="Use NumDomain_hasTruncn.Build instead.")]
Notation Build T U := (NumDomain_hasTruncn.Build T U) (only parsing).
End NumDomain_isArchimedean.


Fact trunc_itv x : 0 ≤ x → (trunc x)%:R ≤ x < (trunc x).+1%:R.

Definition floor (x : R) : int :=
  if 0 ≤ x then Posz (trunc x)
  else if x < 0 then - Posz (trunc (- x) + ~~ int_num x) else 0.

Fact floorP x :
  if x \is Rreal then (floor x)%:~R ≤ x < (floor x + 1)%:~R else floor x == 0.

Fact truncE x : trunc x = if floor x is Posz n then n else 0.

Fact trunc_def x n : n%:R ≤ x < n.+1%:R → trunc x = n.

Fact natrK : cancel (GRing.natmul 1) trunc.

Fact intrP x : reflect (∃ n, x = n%:~R) (int_num x).

Fact natrP x : reflect (∃ n, x = n%:R) (nat_num x).




  Implicit Type x : R.

  Definition bound x := sval (sigW (archi_bound_subproof x)).

  Lemma boundP x : 0 ≤ x → x < (bound x)%:R.

  Fact truncn_subproof x : {m | 0 ≤ x → m%:R ≤ x < m.+1%:R }.

  Definition truncn x := if 0 ≤ x then sval (truncn_subproof x) else 0%N.

  Lemma truncnP x :
    if 0 ≤ x then (truncn x)%:R ≤ x < (truncn x).+1%:R else truncn x == 0%N.


Module Exports. End Exports.

Not to pollute the local namespace, we define Num.nat and Num.int here.
Notation nat := nat_num.
Notation int := int_num.

#[deprecated(since="mathcomp 2.3.0", note="Use Num.ArchiRealDomain instead.")]
Notation ArchiDomain T := (ArchiRealDomain T).
Module ArchiDomain.
#[deprecated(since="mathcomp 2.3.0",
  note="Use Num.ArchiRealDomain.type instead.")]
Notation type := ArchiRealDomain.type.
#[deprecated(since="mathcomp 2.3.0",
  note="Use Num.ArchiRealDomain.copy instead.")]
Notation copy T C := (ArchiRealDomain.copy T C).
#[deprecated(since="mathcomp 2.3.0",
  note="Use Num.ArchiRealDomain.on instead.")]
Notation on T := (ArchiRealDomain.on T).
End ArchiDomain.
#[deprecated(since="mathcomp 2.3.0", note="Use Num.ArchiRealField instead.")]
Notation ArchiField T := (ArchiRealField T).
Module ArchiField.
#[deprecated(since="mathcomp 2.3.0",
  note="Use Num.ArchiRealField.type instead.")]
Notation type := ArchiRealField.type.
#[deprecated(since="mathcomp 2.3.0",
  note="Use Num.ArchiRealField.copy instead.")]
Notation copy T C := (ArchiRealField.copy T C).
#[deprecated(since="mathcomp 2.3.0", note="Use Num.ArchiRealField.on instead.")]
Notation on T := (ArchiRealField.on T).
End ArchiField.

#[deprecated(since="mathcomp 2.3.0", note="Use real_floorDzr instead.")]
Notation floorD := real_floorDzr.
#[deprecated(since="mathcomp 2.3.0", note="Use real_ceilDzr instead.")]
Notation ceilD := real_ceilDzr.
#[deprecated(since="mathcomp 2.3.0", note="Use real_ceilDzr instead.")]
Notation real_ceilD := real_ceilDzr.

End Num.

Export Num.Exports.

#[deprecated(since="mathcomp 2.3.0", note="Use archiRealDomainType instead.")]
Notation archiDomainType := archiRealDomainType (only parsing).
#[deprecated(since="mathcomp 2.3.0", note="Use archiRealFieldType instead.")]
Notation archiFieldType := archiRealFieldType (only parsing).