Remove duplicated lemmas and dependency to Rstruct #1347
Conversation
| @@ -3708,7 +3640,7 @@ 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}. | |||
|
|
|||
| Let normal_spaceP : [<-> | |||
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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?)
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...
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
We should maybe keep an issue with a permalink to the incriminated proof after merge to keep track of this need.
There was a problem hiding this comment.
Opened #1355 to remember (and added a comment in the code)
proux01
force-pushed
the
rm_duplication
branch
from
f4c1c83 to
5c86651
Compare
|
So this should now be ready |
|
So @affeldt-aist should this be merged? |
Motivation for this change
This both removes copy/pasted lemmas (the removed lemmas are still in Rstruct.v) and an undue dependency to Rstruct.
Checklist
[ ] added corresponding entries inCHANGELOG_UNRELEASED.md[ ] added corresponding documentation in the headersReference: How to document
Reminder to reviewers