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 <= z < (m + 1)%:~R when x \is a Num.real, otherwise 0%Z Num.ceil x == the m : int such that (m - 1)%:~R < z <= m%:~R when x \is a NUm.real, otherwise 0%Z Num.trunc x == the n : nat such that n%:R <= z < 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 ssrnum.Num.

#[short (type ="archiNumDomainType")]
HB.structure Definition ArchiNumDomain :=
  { R of NumDomain_isArchimedean R & NumDomain R }.

Module ArchiNumDomainExports.
Bind Scope ring_scope with ArchiNumDomain.sort.
End ArchiNumDomainExports.

#[short (type ="archiNumFieldType")]
HB.structure Definition ArchiNumField :=
  { R of NumDomain_isArchimedean R & NumField R }.

Module ArchiNumFieldExports.
Bind Scope ring_scope with ArchiNumField.sort.
End ArchiNumFieldExports.

#[short (type ="archiClosedFieldType")]
HB.structure Definition ArchiClosedField :=
  { R of NumDomain_isArchimedean R & ClosedField R }.

Module ArchiClosedFieldExports.
Bind Scope ring_scope with ArchiClosedField.sort.
End ArchiClosedFieldExports.

#[short (type ="archiRealDomainType")]
HB.structure Definition ArchiRealDomain :=
  { R of NumDomain_isArchimedean R & RealDomain R }.

Module ArchiRealDomainExports.
Bind Scope ring_scope with ArchiRealDomain.sort.
End ArchiRealDomainExports.

#[short (type ="archiRealFieldType")]
HB.structure Definition ArchiRealField :=
  { R of NumDomain_isArchimedean R & RealField R }.

Module ArchiRealFieldExports.
Bind Scope ring_scope with ArchiRealField.sort.
End ArchiRealFieldExports.

#[short (type ="archiRcfType")]
HB.structure Definition ArchiRealClosedField :=
  { R of NumDomain_isArchimedean R & RealClosedField R }.

Module ArchiRealClosedFieldExports.
Bind Scope ring_scope with ArchiRealClosedField.sort.
End ArchiRealClosedFieldExports.

Module Import Def.
Export ssrnum.Num.Def.
Section Def.
Context {R : archiNumDomainType}.
Implicit Types x : R.

Definition trunc : R → nat := @trunc_subdef R.
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 ].

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

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

Local Fact floor_subproof x :
  {m | if x \is Rreal then m %:~R ≤ x < (m + 1)%:~R else m == 0}.

Definition floor x := sval (floor_subproof x).
Definition ceil x := - floor (- x).
Definition archi_bound x := (trunc `|x |).+1.

End Def.
End Def.

Arguments trunc {R} : simpl never.
Arguments nat_num {R} : simpl never.
Arguments int_num {R} : simpl never.

Notation trunc := trunc.
Notation floor := floor.
Notation ceil := ceil.
Notation bound := archi_bound.

Module intArchimedean.
Section intArchimedean.

Implicit Types n : int.

Let trunc n : nat := if n is Posz n' then n' else 0%N.

Lemma truncP n :
  if 0 ≤ n then (trunc n )%:R ≤ n < (trunc n ).+1 %:R else trunc n == 0%N.

Lemma is_natE n : (0 ≤ n ) = ((trunc n )%:R == n ).

Lemma is_intE n : true = (0 ≤ n ) || (0 ≤ - n ).

End intArchimedean.
End intArchimedean.

#[export ]
HB.instance Definition _ := NumDomain_isArchimedean.Build int
  intArchimedean.truncP intArchimedean.is_natE intArchimedean.is_intE.

Module Import Theory.
Export ssrnum.Num.Theory.

Section ArchiNumDomainTheory.

Variable R : archiNumDomainType.
Implicit Types x y z : R.

Local Notation trunc := (@trunc R).
Local Notation floor := (@floor R).
Local Notation ceil := (@ceil R).
Local Notation nat_num := (@nat_num R).
Local Notation int_num := (@int_num R).

trunc and nat_num

Definition trunc_itv x : 0 ≤ x → (trunc x )%:R ≤ x < (trunc x ).+1 %:R :=
  @Def.trunc_itv R x.

Lemma natrE x : (x \is a nat_num ) = ((trunc x )%:R == x ).

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

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

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

Lemma truncK : {in nat_num , cancel trunc (GRing.natmul 1)}.

Lemma trunc0 : trunc 0 = 0%N.
Lemma trunc1 : trunc 1 = 1%N.
#[local] Hint Resolve trunc0 trunc1 : core.

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

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

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

Lemma truncM : {in nat_num &, {morph trunc : x y / x × y >-> (x × y)%N}}.

Lemma truncX n : {in nat_num , {morph trunc : x / x ^+ n >-> (x ^ n)%N}}.

Lemma rpred_nat_num (S : semiringClosed R) x : x \is a nat_num → x \in S.

Lemma nat_num0 : 0 \is a nat_num.
Lemma nat_num1 : 1 \is a nat_num.
#[local] Hint Resolve nat_num0 nat_num1 : core.

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 natr_normK x : x \is a nat_num → `|x | ^+ 2 = x ^+ 2.

Lemma trunc_gt0 x : (0 < trunc x)%N = (1 ≤ x ).

Lemma trunc0Pn x : reflect (trunc x = 0%N) (~~ (1 ≤ x )).

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 norm_natr x : x \is a nat_num → `|x | = x.

Lemma sum_truncK I r (P : pred I) F : (∀ i, P i → F i \is a nat_num ) →
  (\sum_(i <- r | P i ) trunc (F i))%:R = \sum_(i <- r | P i ) F i.

Lemma prod_truncK I r (P : pred I) F : (∀ i, P i → F i \is a nat_num ) →
  (\prod_(i <- r | P i ) trunc (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.

floor and int_num

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

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

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

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

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

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

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

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

Lemma intrKfloor : cancel intr floor.

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

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

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

ceil and int_num

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

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

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

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

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

Lemma ceil_le : {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_floor x : x \is Rreal →
ceil x = floor x + (~~ (x \is a int_num )).

Lemma rpred_int_num (S : subringClosed R) x : x \is a int_num → x \in S.

Lemma int_num0 : 0 \is a int_num.
Lemma int_num1 : 1 \is a int_num.
#[local] Hint Resolve int_num0 int_num1 : core.

Fact int_num_subring : subring_closed int_num.
#[export ]
HB.instance