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. NB: the Archimedean structures are actually defined in ssrnum, but they are deprecated in ssrnum and will be relocated to this file in a future release. 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. archiDomainType == realDomainType with the Archimedean axiom The HB class is called ArchiDomain. archiFieldType == realFieldType with the Archimedean axiom The HB class is called ArchiField. 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.

Module Import Exports.

Notation archiNumDomainType := Num.ArchiNumDomain.type.
Notation archiNumFieldType := Num.ArchiNumField.type.
Notation archiClosedFieldType := Num.ArchiClosedField.type.
Notation archiDomainType := Num.ArchiDomain.type.
Notation archiFieldType := Num.ArchiField.type.
Notation archiRcfType := Num.ArchiRealClosedField.type.

End Exports.

Module Import Internals.

Section ArchiNumDomain.
Variable R : archiNumDomainType.
Implicit Types x y : R.

Local Notation trunc := (@Num.Def.trunc R).

Definition truncP x :
  if 0 ≤ x then (trunc x )%:R ≤ x < (trunc x ).+1 %:R else trunc x == 0%N :=
  Num.Internals.truncP x.

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

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

End ArchiNumDomain.

End Internals.

Module Import Def.
Export ssrnum.Num.Def.
Definition floor {R : archiNumDomainType} (x : R) := sval (floor_subproof x).
Definition ceil {R : archiNumDomainType} (x : R) := - floor (- x).
End Def.

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

Module Import Theory.
Export ssrnum.Num.Theory.

Section ArchiNumDomainTheory.

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

Local Notation trunc := (@Num.trunc R).
Local Notation floor := (@Num.floor R).
Local Notation ceil := (@Num.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 :=
  @trunc_itv R x.

Definition natrE x : (x \is a nat_num ) = ((trunc x )%:R == x ) :=
  @ssrnum.Num.Theory.mc_2_0.natrE R x.

Definition archi_boundP x : 0 ≤ x → x < (bound x )%:R :=
  @ssrnum.Num.Theory.mc_2_0.archi_boundP R x.

Definition trunc_def x n : n %:R ≤ x < n .+1 %:R → trunc x = n :=
  @ssrnum.Num.Theory.mc_2_0.trunc_def R x n.

Definition natrK : cancel (GRing.natmul 1) trunc :=
  @ssrnum.Num.Theory.mc_2_0.natrK R.

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.

Definition natr_nat n : n %:R \is a nat_num :=
  @ssrnum.Num.Theory.mc_2_0.natr_nat R n.
#[local] Hint Resolve natr_nat : core.

Definition natrP x : reflect (∃ n , x = n %:R) (x \is a nat_num) :=
  @ssrnum.Num.Theory.mc_2_0.natrP R x.

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.

Definition nat_num0 : 0 \is a nat_num := @ssrnum.Num.Theory.mc_2_0.nat_num0 R.
Definition nat_num1 : 1 \is a nat_num := @ssrnum.Num.Theory.mc_2_0.nat_num1 R.
#[local] Hint Resolve nat_num0 nat_num1 : core.

Definition nat_num_semiring : semiring_closed nat_num :=
  @ssrnum.Num.Theory.mc_2_0.nat_num_semiring R.
#[export ]
HB.instance Definition _ := GRing.isSemiringClosed.Build R Num.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%N.

Definition intrE x : (x \is a int_num ) = (x \is a nat_num ) || (- x \is a nat_num ) :=
  @ssrnum.Num.Theory.mc_2_0.intrE R x.

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

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

Lemma 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 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 floorD : {in int_num & Rreal , {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 ceil_itv x : x \is Rreal → (ceil x - 1)%:~R < x ≤ (ceil x )%:~R.

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

Lemma 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 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 ceilD : {in int_num & Rreal , {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 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.
Definition int_num1 : 1 \is a int_num := @ssrnum.Num.Theory.mc_2_0.int_num1 R.
#[local] Hint Resolve int_num0 int_num1 : core.

Fact int_num_subring : subring_closed int_num.
#[export ]
HB.instance Definition _ := GRing.isSubringClosed.Build R Num.int_num_subdef
int_num_subring.

Lemma intr_nat : {subset nat_num ≤ int_num }.

Lemma Rreal_int : {subset int_num ≤ Rreal }.

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

Lemma intrEsign x : x \is a int_num → x = (-1) ^+ (x < 0)%R × `|x |.

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

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

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

Relating Cnat and oldCnat.

Lemma trunc_floor x : trunc x = if 0 ≤ x then `|floor x |%N else 0%N.

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.

Arguments natrK {R} _%N.
Arguments intrKfloor {R}.
Arguments intrKceil {R}.
Arguments natrP {R x}.
Arguments intrP {R x}.
#[global] Hint Resolve trunc0 trunc1 : 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 Num.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 Num.int_num_subdef)) ⇒ apply: intr_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 Num.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 Num.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 Num.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 Num.int_num_subdef)) ⇒ apply: int_num1 : core.

Section ArchiDomainTheory.

Variables (R : archiDomainType).

Definition upper_nthrootP (x : R) i : (bound x ≤ i)%N → x < 2%:R ^+ i :=
@ssrnum.Num.Theory.mc_2_0.upper_nthrootP R x i.

End ArchiDomainTheory.

Section ArchiNumFieldTheory.

Variable R : archiNumFieldType.

autLmodC

Implicit Type nu : {rmorphism R → R }.

Lemma natr_aut nu x : (nu x \is a nat_num ) = (x \is a nat_num ).

Lemma intr_aut nu 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.

Notation Znat_def := ssrint.mc_2_0.Znat_def.
Notation ZnatP := ssrint.mc_2_0.ZnatP.

End ZnatPred.

End Theory.

Module PredInstances.
End PredInstances.

Notation nat := nat_num.
Notation int := int_num.

End Num.

Export Num.ArchiNumDomain.Exports Num.ArchiNumField.Exports.
Export Num.ArchiClosedField.Exports Num.ArchiDomain.Exports.
Export Num.ArchiField.Exports Num.ArchiRealClosedField.Exports.
Export Num.Exports Num.PredInstances.