Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove duplicated lemmas and dependency to Rstruct #1347

Merged
merged 1 commit into from
Oct 17, 2024
Merged

Remove duplicated lemmas and dependency to Rstruct #1347

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 13 additions & 76 deletions theories/normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import archimedean.
From mathcomp Require Import cardinality set_interval Rstruct.
From mathcomp Require Import cardinality set_interval.
Require Import ereal reals signed topology prodnormedzmodule function_spaces.
Require Export separation_axioms.

Expand Down Expand Up @@ -1101,74 +1101,6 @@ Arguments cvgr0_norm_le {_ _ _ F FF}.
note="use `cvgrPdist_lt` or a variation instead")]
Notation cvg_distP := fcvgrPdist_lt (only parsing).

(* NB: the following section used to be in Rstruct.v *)
Require Rstruct.

Section analysis_struct.

Import Rdefinitions.
Import Rstruct.

(* TODO: express using ball?*)
Lemma continuity_pt_nbhs (f : R -> R) x :
Ranalysis1.continuity_pt f x <->
forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num).
Proof.
split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
have [_/posnumP[d] xd_fxe] := fcont e.
exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num].
by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
have /RltP egt0 := [gt0 of e%:num].
have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney].
by rewrite subrr normr0.
apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
by have /RltP := xyd; rewrite distrC.
Qed.

Lemma continuity_pt_cvg (f : R -> R) (x : R) :
Ranalysis1.continuity_pt f x <-> {for x, continuous f}.
Proof.
eapply iff_trans; first exact: continuity_pt_nbhs.
apply iff_sym.
have FF : Filter (f @ x).
by typeclasses eauto.
(*by apply fmap_filter; apply: @filter_filter (locally_filter _).*)
case: (@fcvg_ballP _ _ (f @ x) FF (f x)) => {FF}H1 H2.
(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
split => [{H2} - /H1 {}H1 eps|{H1} H].
- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
exists x0%:num => //= Hx0' /Hx0 /=.
by rewrite /= distrC; apply.
- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0].
exists x0%:num => //= y /Hx0 /= {}Hx0.
by rewrite /ball /= distrC.
Qed.

Lemma continuity_ptE (f : R -> R) (x : R) :
Ranalysis1.continuity_pt f x <-> {for x, continuous f}.
Proof. exact: continuity_pt_cvg. Qed.

Local Open Scope classical_set_scope.

Lemma continuity_pt_cvg' f x :
Ranalysis1.continuity_pt f x <-> f @ x^' --> f x.
Proof. by rewrite continuity_ptE continuous_withinNx. Qed.

Lemma continuity_pt_dnbhs f x :
Ranalysis1.continuity_pt f x <->
forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps).
Proof.
rewrite continuity_pt_cvg' (@cvgrPdist_lt _ [the normedModType _ of R^o]).
exact.
Qed.

Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) :
nbhs (f x) P -> Ranalysis1.continuity_pt f x -> \near x, P (f x).
Proof. by move=> Lf /continuity_pt_cvg; apply. Qed.

End analysis_struct.

Section nbhs_lt_le.
Context {R : realType}.
Implicit Types x z : R.
Expand Down Expand Up @@ -3708,16 +3640,17 @@ exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split.
Qed.

Section normalP.
Context {T : topologicalType}.
Context {R : realType} {T : topologicalType}.

(* Ideally, R should be an instance of realType here,
rather than a section variable. *)
Let normal_spaceP : [<->
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So the reason I didn't do this before is that none of the clauses in normal_spaceP actually depend on R. It's only used internally in the proofs. So if there's a preferred way to show that there is an instance of realType, that would be great. If not then I am ok with this change if removing the dependency is helpful.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the explanation, I see what you intended there now. But while this makes perfect sense from a mathematical point of view, it seems much more dubiuous from a software engineering point of view. This dependency to Rstruct pull a complete dependency to the Stdlib, that is 200k+ lines of code (something about the size of mathcomp) and a bunch of specific axioms (that you can see with Print Assumptions).
Indeed, the goal of Rstruct.v is not to provide an instance of realType (although it incidentally does) but rather to provide a bridge between Analysis and the reals from Stdlib.
I guess providing an instance of realType was the goal of the developments in altreals but this never got completed. @affeldt-aist @CohenCyril what's your opinion?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess providing an instance of realType was the goal of the developments in altreals but this never got completed. @affeldt-aist @CohenCyril what's your opinion?

That's a tough one. I think that @drouhling and @CohenCyril worked hard to remove the dependency to R in topology.v, that's a different problem, sure, but in the same vein I think that the end-user might not want to see such a dependency if does not appear explicitly in the clauses of the statement.

Would the availability of a model relying only on MathComp-Analysis be a good compromise? Because @strub started the following one (@proux01 : by any chance, are referring to this when you talk about the goal of altreals?)

#116

iirc the work was on the verge of completion. It is maybe time to reboot it, we have been postponing it from one release to the other for a long time...

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe, my understanding of altreals is very poor.
Indeed, it would be good to complete a proper instance of realType. That may also be a good thing for users avoinding them to always need that strange Variable R : realType everywhere in the code.
Meanwhile, maybe a good compromise for this PR is to keep a comment mentioning that we should use that instance as soon as we get it?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A MCA only instance of the reals would be the nicest solution here. But in the meanwhile the extra R parameter seems a small price to pay for the removing that dependency.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should maybe keep an issue with a permalink to the incriminated proof after merge to keep track of this need.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Opened #1355 to remember (and added a comment in the code)

(* 0 *) normal_space T;
(* 1 *) forall (A B : set T), closed A -> closed B -> A `&` B = set0 ->
uniform_separator A B;
(* 2 *) forall (A B : set T), closed A -> closed B -> A `&` B = set0 ->
exists U V, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0] ].
Proof.
pose R := Rdefinitions.R.
tfae; first by move=> ?; exact: normal_uniform_separator.
- move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R).
case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1].
Expand Down Expand Up @@ -3755,25 +3688,29 @@ End normalP.

Section completely_regular.

Definition completely_regular_space {R : realType} {T : topologicalType} :=
Context {R : realType}.

Definition completely_regular_space {T : topologicalType} :=
forall (a : T) (B : set T), closed B -> ~ B a -> exists f : T -> R, [/\
continuous f,
f a = 0 &
f @` B `<=` [set 1] ].

(* Ideally, R should be an instance of realType here,
rather than a section variable. *)
Lemma point_uniform_separator {T : uniformType} (x : T) (B : set T) :
closed B -> ~ B x -> uniform_separator [set x] B.
Proof.
move=> clB nBx; have : open (~` B) by rewrite openC.
rewrite openE => /(_ _ nBx); rewrite /interior /= -nbhs_entourageE.
case=> E entE EnB.
pose T' := [the pseudoMetricType Rdefinitions.R of gauge.type entE].
pose T' : pseudoMetricType R := gauge.type entE.
exists (Uniform.class T); exists E; split => //; last by move => ?.
by rewrite -subset0 => -[? w [/= [-> ? /xsectionP ?]]]; exact: (EnB w).
Qed.

Lemma uniform_completely_regular {R : realType} {T : uniformType} :
@completely_regular_space R T.
Lemma uniform_completely_regular {T : uniformType} :
@completely_regular_space T.
Proof.
move=> x B clB Bx.
have /(@uniform_separatorP _ R) [f] := point_uniform_separator clB Bx.
Expand Down Expand Up @@ -3815,7 +3752,7 @@ Qed.
Lemma pseudometric_normal {R : realType} {X : pseudoMetricType R} :
normal_space X.
Proof.
apply/normal_openP => A B clA clB AB0.
apply/(@normal_openP R) => A B clA clB AB0.
have eps' (D : set X) : closed D -> forall x, exists eps : {posnum R}, ~ D x ->
ball x eps%:num `&` D = set0.
move=> clD x; have [nDx|?] := pselect (~ D x); last by exists 1%:pos.
Expand Down
2 changes: 1 addition & 1 deletion theories/numfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -480,7 +480,7 @@ Lemma urysohn_ext_itv A B x y :
f @` A `<=` [set x], f @` B `<=` [set y] & range f `<=` `[x, y]].
Proof.
move=> cA cB A0 xy; move/normal_separatorP : normalX => urysohn_ext.
have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext _ _ cA cB A0.
have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext R _ _ cA cB A0.
pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=.
move=> t; apply: continuous_comp; first exact: cf.
apply: (@continuousD R R^o).
Expand Down