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 Definition _ := GRing.isSubringClosed.Build R 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 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 (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 : (archi_bound x ≤ i)%N → x < 2%:R ^+ i.

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

Lemma ge_floor x : (floor x )%:~R ≤ x.

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

Lemma floor_ge_int x n : n %:~R ≤ x = (n ≤ floor x ).

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 ceil_itv x : (ceil x - 1)%:~R < x ≤ (ceil x )%:~R.

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

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

Lemma ceil_le_int x n : x ≤ n %:~R = (ceil x ≤ n ).

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

End ArchiRealDomainTheory.

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.

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.

  Implicit Type x : R.

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

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

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

  Definition trunc x := if 0 ≤ x then sval (trunc_subproof x) else 0%N.

  Lemma truncP x :
    if 0 ≤ x then (trunc x )%:R ≤ x < (trunc x ).+1 %:R else trunc 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).