Files

Module mathcomp.reals_stdlib.Rstruct

From Stdlib Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
From Stdlib Require Import Rtrigo1 Reals.
From HB Require Import structures.
From mathcomp Require Import boot order ssralg poly ssrnum archimedean.


# Compatibility with the real numbers of Stdlib This essentially builds an instance of realType for the R type from the Stdlib library. This enables specializing all proofs on realType (that is, many things in the Analysis library) to Stdlib's real numbers. To this end, one can use tactics like `apply: RleP` or `rewrite !RealsE` (see below for more compatibility lemmas).


Unset SsrOldRewriteGoalsOrder.  
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope R_scope.

Lemma Req_EM_TSource code (r1Source code r2Source code : R) : {r1 = r2} + {r1 <> r2}.
Proof.
case: (total_order_T r1 r2) => [[r1Lr2 | <-] | r1Gr2].
- by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {2}r1Er2.
- by left.
by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {1}r1Er2.
Qed.

Definition eqr
Source code (r1Source code r2Source code : R) : bool :=
  if Req_EM_T r1 r2 is left _ then true else false.

Lemma eqrPSource code : Equality.axiom eqr.
Proof.
by move=> r1 r2; rewrite /eqr; case: Req_EM_T=> H; apply: (iffP idP).
Qed.

#[hnf]Source code HBSource code.instanceSource code DefinitionSource code _Source code :=Source code hasDecEqSource code.Build R eqrP.

Fact inhRSource code : inhabited R.
Proof.
exact: (inhabits 0). Qed.

Definition pickR
Source code (PSource code : pred R) (nSource code : nat) :=
  let xSource code := epsilon inhR P in if P x then Some x else None.

Fact pickR_someSource code PSource code nSource code xSource code : pickR P n = Some x -> P x.
Proof.
by rewrite /pickR; case: (boolP (P _)) => // Px [<-]. Qed.

Fact pickR_exSource code (PSource code : pred R) :
  (exists xSource code : R, P x) -> exists nSource code, pickR P n.
Proof.
by rewrite /pickR; move=> /(epsilon_spec inhR)->; exists 0%N. Qed.

Fact pickR_extSource code (PSource code QSource code : pred R) : P =1 Q -> pickR P =1 pickR Q.
Proof.
move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _.
suff->: u = v by rewrite PEQ.
by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ.
Qed.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code hasChoiceSource code.Build R pickR_some pickR_ex pickR_ext.

Fact RplusASource code : associative (Rplus).
Proof.
by move=> *; rewrite Rplus_assoc. Qed.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.isZmodule.Build R
  RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Fact RmultASource code : associative Rmult.
Proof.
by move=> *; rewrite Rmult_assoc. Qed.

Fact R1_neq_0Source code : R1 != R0.
Proof.
by apply/eqP/R1_neq_R0. Qed.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.Zmodule_isNzRing.Build R
  RmultA Rmult_1_l Rmult_1_r Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.SemiRing_hasCommutativeMul.Build R Rmult_comm.

Import Monoid.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isComLawSource code.Build R 0 Rplus
  RplusA Rplus_comm Rplus_0_l.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isComLawSource code.Build R 1 Rmult
  RmultA Rmult_comm Rmult_1_l.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMulLawSource code.Build R 0 Rmult Rmult_0_l Rmult_0_r.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isAddLawSource code.Build R Rmult Rplus
  Rmult_plus_distr_r Rmult_plus_distr_l.

Definition unit_R

eqr : R -> R -> bool eqr is not universe polymorphic Arguments eqr (r1 r2)%_R_scope eqr is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.eqr Declared in library mathcomp.reals_stdlib.Rstruct, line 58, characters 11-14

Source code rSource code := r != 0.

Lemma intro_unit_RSource code xSource code ySource code : y * x = 1 /\ x * y = 1 -> unit_R x.
Proof.
move=> [yx_eq1 _]; apply: contra_eqN yx_eq1 => /eqP->.
by rewrite Rmult_0_r eq_sym R1_neq_0.
Qed.

Section Rinvx.

Let RinvxSource code rSource code := if r != 0 then / r else r.

Let neq0_RinvxESource code xSource code : x != 0 -> Rinv x = Rinvx x.
Proof.
by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed.

Let RinvxESource code xSource code : Rinv x = Rinvx x.
Proof.
have [->| ] := eqVneq x R0; last exact: neq0_RinvxE.
rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=.
rewrite RinvImpl.Rinv_def; case: Req_appart_dec => //.
by move=> /[dup] -[] /Rlt_irrefl.
Qed.

Lemma RmultRinvSource code : {in unit_R, left_inverse 1 Rinv Rmult}.
Proof.
move=> r; rewrite RinvxE -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_l //; apply/eqP.
Qed.

Lemma RinvRmultSource code : {in unit_R, right_inverse 1 Rinv Rmult}.
Proof.
move=> r; rewrite RinvxE -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_r //; apply/eqP.
Qed.

Lemma Rinv_outSource code : {in predC unit_R, Rinv =1 id}.
Proof.
by move=> x; rewrite inE/= RinvxE /Rinvx -if_neg => ->. Qed.

End Rinvx.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.NzRing_hasMulInverse.Build R
  RmultRinv RinvRmult intro_unit_R Rinv_out.

Lemma R_idomainMixinSource code xSource code ySource code : x * y = 0 -> (x == 0) || (y == 0).
Proof.
by move=> /Rmult_integral []->; rewrite eqxx ?orbT. Qed.

#[hnf]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.ComUnitRing_isIntegral.Build R
  R_idomainMixin.

Lemma R_fieldMixinSource code : GRing.field_axiom R
Proof.
by []. Qed.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code GRingSource code.UnitRing_isField.Build R R_fieldMixin.

Reflect the order on the reals to bool

Definition Rleb

pickR : pred R -> nat -> option R pickR is not universe polymorphic Arguments pickR P n%_nat_scope pickR is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.pickR Declared in library mathcomp.reals_stdlib.Rstruct, line 71, characters 11-16

Source code r1Source code r2Source code := if Rle_dec r1 r2 is left _ then true else false.
Definition Rltb

unit_R : RbaseSymbolsImpl_R__canonical__eqtype_Equality -> bool unit_R is not universe polymorphic Arguments unit_R r unit_R is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.unit_R Declared in library mathcomp.reals_stdlib.Rstruct, line 123, characters 11-17

Source code r1Source code r2Source code := Rleb r1 r2 && (r1 != r2).
Definition Rgeb

Rleb : R -> R -> bool Rleb is not universe polymorphic Arguments Rleb (r1 r2)%_R_scope Rleb is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.Rleb Declared in library mathcomp.reals_stdlib.Rstruct, line 179, characters 11-15

Source code r1Source code r2Source code := Rleb r2 r1.
Definition Rgtb

Rltb : R -> R -> bool Rltb is not universe polymorphic Arguments Rltb (r1 r2)%_R_scope Rltb is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.Rltb Declared in library mathcomp.reals_stdlib.Rstruct, line 180, characters 11-15

Source code r1Source code r2Source code := Rltb r2 r1.

Lemma RlebPSource code r1Source code r2Source code : reflect (r1 <= r2) (Rleb r1 r2).
Proof.
by rewrite /Rleb; apply: (iffP idP); case: Rle_dec. Qed.

Lemma RltbPSource code r1Source code r2Source code : reflect (r1 < r2) (Rltb r1 r2).
Proof.
rewrite /Rltb /Rleb; apply: (iffP idP); case: Rle_dec=> //=.
- by case=> // r1Er2 /eqP[].
- by move=> _ r1Lr2; apply/eqP/Rlt_not_eq.
by move=> Nr1Lr2 r1Lr2; case: Nr1Lr2; left.
Qed.


Section ssreal_struct.

Local Open Scope R_scope.

Lemma Rleb_norm_addSource code xSource code ySource code : Rleb (Rabs (x + y)) (Rabs x + Rabs y).
Proof.
by apply/RlebP/Rabs_triang. Qed.

Lemma addr_Rgtb0Source code xSource code ySource code : Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y).
Proof.
by move/RltbP=> Hx /RltbP Hy; apply/RltbP/Rplus_lt_0_compat. Qed.

Lemma Rnorm0_eq0Source code xSource code : Rabs x = 0 -> x = 0.
Proof.
by move=> H; case: (x == 0) /eqP=> // /Rabs_no_R0. Qed.

Lemma Rleb_leVgeSource code xSource code ySource code : Rleb 0 x -> Rleb 0 y -> (Rleb x y) || (Rleb y x).
Proof.
move/RlebP=> Hx /RlebP Hy; case: (Rlt_le_dec x y).
by move/Rlt_le/RlebP=> ->.
by move/RlebP=> ->; rewrite orbT.
Qed.

Lemma RnormMSource code : {morph Rabs : xSource code ySource code / x * y}.
Proof.
exact: Rabs_mult. Qed.

Lemma Rleb_defSource code xSource code ySource code : (Rleb x y) = (Rabs (y - x) == y - x).
Proof.
apply/(sameP (RlebP x y))/(iffP idP)=> [/eqP H| /Rle_minus H].
  apply: Rminus_le; rewrite -Ropp_minus_distr.
  apply/Rge_le/Ropp_0_le_ge_contravar.
  by rewrite -H; apply: Rabs_pos.
apply/eqP/Rabs_pos_eq.
rewrite -Ropp_minus_distr.
by apply/Ropp_0_ge_le_contravar/Rle_ge.
Qed.

Lemma Rltb_defSource code xSource code ySource code : (Rltb x y) = (y != x) && (Rleb x y).
Proof.
apply/(sameP (RltbP x y))/(iffP idP).
  case/andP=> /eqP H /RlebP/Rle_not_gt H2.
  by case: (Rtotal_order x y)=> // [][] // /esym.
move=> H; apply/andP; split; [apply/eqP|apply/RlebP].
  exact: Rgt_not_eq.
exact: Rlt_le.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code NumSource code.IntegralDomain_isNumRing.Build R
  Rleb_norm_add addr_Rgtb0 Rnorm0_eq0 Rleb_leVge RnormM Rleb_def Rltb_def.

Lemma RlePUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code : forall xSource code ySource code, reflect (Rle x y) (x <= y)%R.
Proof.
exact: RlebP. Qed.
Lemma RltPUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code : forall xSource code ySource code, reflect (Rlt x y) (x < y)%R.
Proof.
exact: RltbP. Qed.

Lemma Rreal_axiomSource code (xSource code : R) : (0 <= x)%R || (x <= 0)%R.
Proof.
case: (Rle_dec 0 x)=> [/RleP ->|] //.
by move/Rnot_le_lt/Rlt_le/RleP=> ->; rewrite orbT.
Qed.

Lemma R_totalSource code : total (<=%O : rel R).
Proof.
move=> x y; case: (Rle_lt_dec x y) => [/RleP -> //|/Rlt_le/RleP ->];
  by rewrite orbT.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code OrderSource code.POrder_isTotal.Build _ R R_total.

Lemma Rarchimedean_axiomSource code : Num.archimedean_axiom R.
Proof.
move=> x; exists (Z.abs_nat (up x) + 2)%N.
have [Hx1 Hx2] := archimed x.
have Hz (zSource code : Z) : z = (z - 1 + 1)%Z by rewrite Zplus_comm Zplus_minus.
have Zabs_nat_Zopp z : Z.abs_nat (- z)%Z = Z.abs_nat z by case: z.
apply/RltbP/Rabs_def1.
  apply: (Rlt_trans _ ((Z.abs_nat (up x))%:R)%R); last first.
    rewrite -[((Z.abs_nat _)%:R)%R]Rplus_0_r mulrnDr.
    by apply/Rplus_lt_compat_l/Rlt_0_2.
  apply: (Rlt_le_trans _ (IZR (up x)))=> //.
  elim/(well_founded_ind (Zwf_well_founded 0)): (up x) => z IHz.
  case: (Z_lt_le_dec 0 z) => [zp | zn].
    rewrite [z]Hz plus_IZR Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
    rewrite plusE mulrnDr.
    apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak.
    exact: Zlt_pred.
  apply: (Rle_trans _ (IZR 0)); first exact: IZR_le.
  by apply/RlebP/(ler0n R (Z.abs_nat z)).
apply: (Rlt_le_trans _ (IZR (up x) - 1)).
  apply: Ropp_lt_cancel; rewrite Ropp_involutive.
  rewrite Ropp_minus_distr /Rminus -opp_IZR -{2}(Z.opp_involutive (up x)).
  elim/(well_founded_ind (Zwf_well_founded 0)): (- up x)%Z => z IHz .
  case: (Z_lt_le_dec 0 z) => [zp | zn].
  rewrite [z]Hz Zabs_nat_Zopp plus_IZR.
  rewrite Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
    rewrite plusE -Rplus_assoc -addnA [(_ + 2)%N]addnC addnA mulrnDr.
    apply: Rplus_lt_compat_r; rewrite -Zabs_nat_Zopp.
    apply: IHz; split; first exact: Zlt_le_weak.
    exact: Zlt_pred.
  apply: (Rle_lt_trans _ 1).
    rewrite -{2}[1]Rplus_0_r; apply: Rplus_le_compat_l.
    by rewrite -/(IZR 0); apply: IZR_le.
  rewrite mulrnDr; apply: (Rlt_le_trans _ 2).
    by rewrite -{1}[1]Rplus_0_r; apply/Rplus_lt_compat_l/Rlt_0_1.
  rewrite -[2]Rplus_0_l; apply: Rplus_le_compat_r.
  by apply/RlebP/(ler0n R (Z.abs_nat _)).
apply: Rminus_le.
rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
exact: Rle_minus.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code NumSource code.NumDomain_bounded_isArchimedean.Build R
  Rarchimedean_axiom.

Here are the lemmas that we will use to prove that R has the rcfType structure.

Lemma continuity_eqSource code fSource code gSource code : f =1 g -> continuity f -> continuity g.
Proof.
move=> Hfg Hf x eps Heps.
have [y [Hy1 Hy2]]:= Hf x eps Heps.
by exists y; split=> // z; rewrite -!Hfg; exact: Hy2.
Qed.

Lemma continuity_sumSource code (ISource code : finType) FSource code (PSource code : pred I) :
  (forall iSource code, P i -> continuity (F i)) ->
  continuity (fun xSource code => (\sum_(iSource code | P i) ((F i) x)))%R.
Proof.
move=> H; elim: (index_enum I)=> [|a l IHl].
  set f:= fun _ => _.
  have Hf: (fun xSource code=> 0) =1 f by move=> x; rewrite /f big_nil.
  by apply: (continuity_eq Hf); exact: continuity_const.
set f := fun _ => _.
case Hpa: (P a).
  have Hf: (fun xSource code => F a x + \sum_(iSource code <- l | P i) F i x)%R =1 f.
    by move=> x; rewrite /f big_cons Hpa.
  apply: (continuity_eq Hf); apply: continuity_plus=> //.
  exact: H.
have Hf: (fun xSource code => \sum_(iSource code <- l | P i) F i x)%R =1 f.
  by move=> x; rewrite /f big_cons Hpa.
exact: (continuity_eq Hf).
Qed.

Lemma continuity_expSource code fSource code nSource code : continuity f -> continuity (fun xSource code => (f x)^+ n)%R.
Proof.
move=> Hf; elim: n=> [|n IHn]; first exact: continuity_const.
set g:= fun _ => _.
have Hg: (fun xSource code=> f x * f x ^+ n)%R =1 g.
  by move=> x; rewrite /g exprS.
by apply: (continuity_eq Hg); exact: continuity_mult.
Qed.

Lemma Rreal_closed_axiomSource code : Num.real_closed_axiom R.
Proof.
move=> p a b; rewrite !le_eqVlt.
case Hpa: ((p.[a])%R == 0%R).
  by move=> ? _ ; exists a=> //; rewrite lexx le_eqVlt.
case Hpb: ((p.[b])%R == 0%R).
  by move=> ? _; exists b=> //; rewrite lexx le_eqVlt andbT.
have [->|Hab] := eqVneq a b.
  by move=> _; rewrite eq_sym Hpb (ltNge 0) /=; case/andP=> /ltW ->.
rewrite eq_sym Hpb /=; clear=> /RltbP Hab /andP[/RltbP Hpa /RltbP Hpb].
suff Hcp : continuity (fun xSource code => (p.[x])%R).
  have [z [[Hza Hzb] /eqP Hz2]]:= IVT _ a b Hcp Hab Hpa Hpb.
  by exists z=> //; apply/andP; split; apply/RlebP.
rewrite -[p]coefK poly_def.
set f := fun _ => _.
have Hf: (fun xSource code : R => \sum_(iSource code < size p) (p`_i * x^+i))%R =1 f.
  move=> x; rewrite /f horner_sum.
  by apply: eq_bigr=> i _; rewrite hornerZ hornerXn.
apply: (continuity_eq Hf); apply: continuity_sum=> i _.
apply:continuity_scal; apply: continuity_exp=> x esp Hesp.
by exists esp; split=> // y [].
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code NumSource code.RealField_isClosed.Build R Rreal_closed_axiom.

End ssreal_struct.
Arguments RleP {x y}.
Arguments RltP {x y}.

Local Open Scope ring_scope.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import reals.

Section ssreal_struct_contd.
Implicit Type E : set R.

Lemma is_upper_boundESource code ESource code xSource code : is_upper_bound E x = (ubound E) x.
Proof.
rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
by apply/ubP => y Ey; apply/RleP/h.
Qed.

Lemma boundESource code ESource code : bound E = has_ubound E.
Proof.
by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.

Lemma RcondcompleteSource code ESource code : has_sup E -> {mSource code | isLub E m}.
Proof.
move=> [E0 uE]; have := completeness E; rewrite boundE => /(_ uE E0)[x [E1 E2]].
exists x; split; first by rewrite -is_upper_boundE; apply: E1.
by move=> y; rewrite -is_upper_boundE => /E2/RleP.
Qed.

Lemma Rsupremums_neq0Source code ESource code : has_sup E -> (supremums E !=set0)%classic.
Proof.
by move=> /Rcondcomplete[x [? ?]]; exists x. Qed.

Lemma Rsup_isLubSource code x0Source code ESource code : has_sup E -> isLub E (supremum x0 E).
Proof.
have [-> [/set0P]|E0 hsE] := eqVneq E set0; first by rewrite eqxx.
have [s [Es sE]] := Rcondcomplete hsE.
split => x Ex; first by apply/ge_supremum_Nmem=> //; exact: Rsupremums_neq0.
rewrite /supremum (negbTE E0); case: xgetP => /=.
  by move=> _ -> [_ EsE]; apply/EsE.
by have [y Ey /(_ y)] := Rsupremums_neq0 hsE.
Qed.

Lemma real_sup_adherentSource code x0Source code ESource code (epsSource code : R) : 0 < eps ->
  has_sup E -> exists2 eSource code, E e & (supremum x0 E - eps) < e.
Proof.
move=> eps_gt0 supE; set m := _ - eps; apply: contrapT=> mNsmall.
have : (ubound E) m.
  apply/ubP => y Ey.
  by have /negP := mNsmall (ex_intro2 _ _ y Ey _); rewrite -leNgt.
have [_ /(_ m)] := Rsup_isLub x0 supE.
move => m_big /m_big.
by rewrite -subr_ge0 addrC addKr oppr_ge0 leNgt eps_gt0.
Qed.

Lemma Rsup_ubSource code x0Source code ESource code : has_sup E -> (ubound E) (supremum x0 E).
Proof.
by move=> supE x Ex; apply/ge_supremum_Nmem => //; exact: Rsupremums_neq0.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code ArchimedeanField_isRealSource code.Build R
  (@Rsup_ub (0 : R)) (real_sup_adherent 0).

Implicit Types (x y : R) (m n : nat).





Lemma expR0Source code : exp (0 : R) = 1.
Proof.
by rewrite exp_0. Qed.

Lemma expRDSource code xSource code ySource code : exp x * exp y = exp (x + y).
Proof.
by rewrite exp_plus. Qed.

Lemma expRXSource code xSource code nSource code : exp x ^+ n = exp (x *+ n).
Proof.
elim: n => [|n Ihn]; first by rewrite expr0 mulr0n exp_0.
by rewrite exprS Ihn mulrS expRD.
Qed.

Lemma sinDSource code xSource code ySource code : sin (x + y) = sin x * cos y + cos x * sin y.
Proof.
by rewrite sin_plus. Qed.

Lemma cosDSource code xSource code ySource code : cos (x + y) = (cos x * cos y - sin x * sin y).
Proof.
by rewrite cos_plus. Qed.

Lemma RplusEUsed by
  • mathcomp.analysis_stdlib.showcase.uniform_bigO
Source code xSource code ySource code : Rplus x y = x + y
Proof.
by []. Qed.

Lemma RminusESource code xSource code ySource code : Rminus x y = x - y
Proof.
by []. Qed.

Lemma RmultESource code xSource code ySource code : Rmult x y = x * y
Proof.
by []. Qed.

Lemma RoppESource code xSource code : Ropp x = - x
Proof.
by []. Qed.

Lemma RinvEUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code xSource code : Rinv x = x^-1
Proof.
by []. Qed.

Lemma RdivESource code xSource code ySource code : Rdiv x y = x / y
Proof.
by rewrite /Rdiv. Qed.

Lemma INREUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code nSource code : INR n = n%:R.
Proof.
elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.

Lemma Pos_to_natESource code pSource code : Pos.to_nat p = nat_of_pos p.
Proof.
by elim: p => //= p <-;
  rewrite ?(Pnat.Pos2Nat.inj_xI,Pnat.Pos2Nat.inj_xO) NatTrec.doubleE -mul2n.
Qed.

Lemma R0ESource code : IZR 0 = 0%R
Proof.
by []. Qed.
Lemma R1ESource code : IZR 1 = 1%R
Proof.
by []. Qed.

Note that rewrites using the following lemma `IZRposE` are systematically followed by a rewrite using the lemma `INRE`.
Lemma IZRposESource code (pSource code : positive) : IZR (Z.pos p) = INR (nat_of_pos p).
Proof.
by rewrite -Pos_to_natE INR_IPR. Qed.

Let ge0_RsqrtESource code xSource code : 0 <= x -> sqrt x = Num.sqrt x.
Proof.
move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; first exact/RleP.
by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
Qed.

Lemma RsqrtEUsed by
  • mathcomp.analysis_stdlib.showcase.uniform_bigO
Source code xSource code : sqrt x = Num.sqrt x.
Proof.
set Rx := Rbasic_fun.Rcase_abs x.
have RxE : Rx = Rbasic_fun.Rcase_abs x by [].
rewrite /R_sqrt.sqrt -RxE.
move: RxE; case: Rbasic_fun.Rcase_abs => x0 RxE.
  by rewrite RxE ler0_sqrtr//; exact/ltW/RltP.
by rewrite /Rx -/(R_sqrt.sqrt _) ge0_RsqrtE //; exact/RleP/Rge_le.
Qed.

Lemma RpowEUsed by
  • mathcomp.analysis_stdlib.showcase.uniform_bigO
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code xSource code nSource code : pow x n = x ^+ n.
Proof.
by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.

Lemma RmaxESource code xSource code ySource code : Rmax x y = Num.max x y.
Proof.
case: (lerP x y) => H; first by rewrite Rmax_right //; apply: RlebP.
by rewrite ?ltW // Rmax_left //;  apply/RlebP; move/ltW : H.
Qed.

Lemma RminESource code xSource code ySource code : Rmin x y = Num.min x y.
Proof.
case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
by rewrite ?ltW // Rmin_right //;  apply/RlebP; move/ltW : H.
Qed.

Lemma RabsESource code xSource code : Rabs x = `|x|.
Proof.
by rewrite /Rabs; case: Rcase_abs => [/RltP x0|/Rge_le/RleP x0];
  [rewrite ltr0_norm|rewrite ger0_norm].
Qed.

Lemma RdistEUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code xSource code ySource code : Rdist x y = `|x - y|.
Proof.
by rewrite /Rdist RabsE RminusE. Qed.

Lemma sum_f_R0EUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code fSource code nSource code : sum_f_R0 f n = \sum_(0 <= kSource code < n.+1) f k.
Proof.
elim: n => [|n ih/=]; first by rewrite big_nat1.
by rewrite RplusE big_nat_recr//= ih.
Qed.

Lemma factEUsed by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code nSource code : fact n = n`!.
Proof.
by elim: n => //= n ih; rewrite factS mulSn ih. Qed.

Definition RealsE

RealsE : (forall x y : R, (x + y)%R = (x + y)%R) * (forall x y : R, (x - y)%R = (x - y)%R) * (forall x y : R, (x * y)%R = (x * y)%R) * (forall x : R, (- x)%R = (- x)%R) * (forall x : R, (/ x)%R = x^-1%R) * (forall x y : R, (x / y)%R = (x / y)%R) * (forall n : nat, INR n = n%:R%R) * (0%R = 0%R) * (1%R = 1%R) * (forall p : positive, Pos.to_nat p = nat_of_pos p) * (forall p : positive, IZR (Z.pos p) = INR (nat_of_pos p)) * (forall x : R, sqrt x = sqrtr x) * (forall (x : R) (n : nat), (x ^ n)%R = (x ^+ n)%R) * (forall x y : R, Rmax x y = maxr x y) * (forall x y : R, Rmin x y = minr x y) * (forall x : R, Rabs x = `|x|%R) * (forall x y : R, Rdist x y = `|x - y|%R) * (forall (f : nat -> R) (n : nat), sum_f_R0 f n = (\sum_(0 <= k < n.+1) f k)%R) * (forall n : nat, fact n = n`!) RealsE is not universe polymorphic RealsE is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.RealsE Declared in library mathcomp.reals_stdlib.Rstruct, line 551, characters 11-17

Used by
  • mathcomp.analysis_stdlib.Rstruct_topology
Source code := (RplusE, RminusE, RmultE, RoppE, RinvE, RdivE,
  INRE, R0E, R1E, Pos_to_natE, IZRposE, RsqrtE, RpowE, RmaxE, RminE,
  RabsE, RdistE, sum_f_R0E, factE).

Section bigmaxr.
Context {RSource code : realDomainType}.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Definition bigmaxr

bigmaxr : forall {R : realDomainType}, R -> seq R -> R bigmaxr is not universe polymorphic Arguments bigmaxr {R} r%_ring_scope s%_seq_scope bigmaxr is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.bigmaxr Declared in library mathcomp.reals_stdlib.Rstruct, line 560, characters 11-18

Source code (rSource code : R) sSource code := \big[Num.max/head r s]_(iSource code <- s) i.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_nilSource code (x0Source code : R) : bigmaxr x0 [::] = x0.
Proof.
#[warning="-deprecated"] by rewrite /bigmaxr /= big_nil.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_unSource code (x0Source code xSource code : R) : bigmaxr x0 [:: x] = x.
Proof.
#[warning="-deprecated"] by rewrite /bigmaxr /= big_cons big_nil maxxx.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxrESource code (rSource code : R) sSource code : bigmaxr r s = foldr Num.max (head r s) (behead s).
Proof.
#[warning="-deprecated"]
rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(iSource code <- s) i).
  #[warning="-deprecated"]
  by case: s => //=; rewrite /bigmaxr big_nil.
#[warning="-deprecated"]
case: s => // ? t; rewrite big_cons /bigmaxr.
by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Lemma bigrmax_dfltSource code (xSource code ySource code : R) sSource code : Num.max x (\big[Num.max/x]_(jSource code <- y :: s) j) =
  Num.max x (\big[Num.max/y]_(iSource code <- y :: s) i).
Proof.
elim: s => /= [|h t IH] in x y *.
by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_consSource code (x0Source code xSource code ySource code : R) lrSource code :
  bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).
Proof.
#[warning="-deprecated"]
by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_lerSource code (x0Source code : R) sSource code iSource code :
  (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
Proof.
#[warning="-deprecated"]
rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
  by rewrite big_cons /= le_max lexx.
rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
#[warning="-deprecated"]
by rewrite big_cons bigrmax_dflt le_max orbC IH.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_addrSource code (x0Source code : R) lrSource code (xSource code : R) :
  bigmaxr (x0 + x) (map (fun ySource code : R => y + x) lr) = (bigmaxr x0 lr) + x.
Proof.
#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => [|h t]; first by rewrite !big_nil.
elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl.
#[warning="-deprecated"]
by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_memSource code (x0Source code : R) lrSource code : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
Proof.
#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => // h t _.
elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
#[warning="-deprecated"]
rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
- by rewrite le_max lexx.
- by rewrite lt_max ltxx => ?; rewrite max_r ?IH // ltW.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_mulrSource code (ASource code : finType) (sSource code : seq A) (kSource code : R) (xSource code : A -> R) :
  0 <= k -> bigmaxr 0 (map (fun iSource code => k * x i) s) = k * bigmaxr 0 (map x s).
Proof.
move=> k0; elim: s => /= [|h [/=|h' t ih]].
#[warning="-deprecated"]
by rewrite bigmaxr_nil mulr0.
#[warning="-deprecated"]
by rewrite !bigmaxr_un.
#[warning="-deprecated"]
by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pMr.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_indexSource code (x0Source code : R) lrSource code :
  (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.
Proof.
#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => //= h t _; case: ifPn => // /negbTE H.
#[warning="-deprecated"]
move: (@bigmaxr_mem x0 (h :: t) isT).
by rewrite ltnS index_mem inE /= eq_sym H.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_lerPSource code (x0Source code : R) lrSource code (xSource code : R) :
  (0 < size lr)%N ->
  reflect (forall iSource code, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).
Proof.
move=> lr_size; apply: (iffP idP) => [le_x i i_size | H].
  #[warning="-deprecated"]
  by apply: (le_trans _ le_x); apply: bigmaxr_ler.
#[warning="-deprecated"]
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_ltrPSource code (x0Source code : R) lrSource code (xSource code : R) :
  (0 < size lr)%N ->
  reflect (forall iSource code, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).
Proof.
move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H].
  #[warning="-deprecated"]
  by apply: le_lt_trans lt_x; apply: bigmaxr_ler.
#[warning="-deprecated"]
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxrPSource code (x0Source code : R) lrSource code (xSource code : R) :
  (x \in lr /\ forall iSource code, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).
Proof.
move=> [] /(nthP x0) [] j j_size j_nth x_ler; apply: le_anti; apply/andP; split.
  #[warning="-deprecated"]
  by apply/bigmaxr_lerP => //; apply: (leq_trans _ j_size).
#[warning="-deprecated"]
by rewrite -j_nth (bigmaxr_ler _ j_size).
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bigmaxr_lerifSource code (x0Source code : R) lrSource code :
  uniq lr -> forall iSource code, (i < size lr)%N ->
     (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).
Proof.
#[warning="-deprecated"]
move=> lr_uniq i i_size; rewrite /Num.leif (bigmaxr_ler _ i_size).
#[warning="-deprecated"]
rewrite -(nth_uniq x0 i_size (bigmaxr_index _ (leq_trans _ i_size)) lr_uniq) //.
rewrite nth_index //.
#[warning="-deprecated"]
by apply: bigmaxr_mem; apply: (leq_trans _ i_size).
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Definition bmaxrf

bmaxrf : forall {R : realDomainType} [n : nat], {ffun 'I_n.+1 -> R} -> R bmaxrf is not universe polymorphic Arguments bmaxrf {R} [n]%_nat_scope f bmaxrf is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.bmaxrf Declared in library mathcomp.reals_stdlib.Rstruct, line 730, characters 11-17

Source code nSource code (fSource code : {ffun 'I_n.+1 -> R}) :=
  bigmaxr (f ord0) (codom f).

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bmaxrf_lerSource code nSource code (fSource code : {ffun 'I_n.+1 -> R}) iSource code :
  (f i) <= (bmaxrf f).
Proof.
#[warning="-deprecated"]
move: (@bigmaxr_ler (f ord0) (codom f) (nat_of_ord i)).
#[warning="-deprecated"]
rewrite /bmaxrf size_codom card_ord => H; move: (ltn_ord i); move/H.
suff -> : nth (f ord0) (codom f) i = f i; first by [].
by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bmaxrf_indexSource code nSource code (fSource code : {ffun 'I_n.+1 -> R}) :
  (index (bmaxrf f) (codom f) < n.+1)%N.
Proof.
#[warning="-deprecated"]
rewrite /bmaxrf.
rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)).
  by rewrite size_codom card_ord.
#[warning="-deprecated"]
by apply: bigmaxr_index; rewrite size_codom card_ord.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Definition index_bmaxrf

index_bmaxrf : forall {R : realDomainType} [n : nat], {ffun 'I_n.+1 -> R} -> 'I_n.+1 index_bmaxrf is not universe polymorphic Arguments index_bmaxrf {R} [n]%_nat_scope f index_bmaxrf is transparent Expands to: Constant mathcomp.reals_stdlib.Rstruct.index_bmaxrf Declared in library mathcomp.reals_stdlib.Rstruct, line 761, characters 11-23

Source code nSource code fSource code := Ordinal (@bmaxrf_index n f).

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Lemma ordnatSource code iSource code nSource code (ord_iSource code : (i < n)%N) : i = Ordinal ord_i :> nat.
Proof.
by []. Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma eq_index_bmaxrfSource code nSource code (fSource code : {ffun 'I_n.+1 -> R}) :
  f (index_bmaxrf f) = bmaxrf f.
Proof.
#[warning="-deprecated"]
move: (bmaxrf_index f).
rewrite -[X in _ (_ < X)%N]card_ord -(size_codom f) index_mem.
move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
  #[warning="-deprecated"]
  by rewrite size_enum_ord; apply: bmaxrf_index.
#[warning="-deprecated"]
by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma bmaxrf_lerifSource code nSource code (fSource code : {ffun 'I_n.+1 -> R}) :
  injective f -> forall iSource code,
     (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).
Proof.
#[warning="-deprecated"]
by move=> inj_f i; rewrite /Num.leif bmaxrf_ler -(inj_eq inj_f) eq_index_bmaxrf.
Qed.

End bigmaxr.

End ssreal_struct_contd.
Generated by rocqnavi
Source
Uses
Used By