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
ceil and int_num