WIP / Experiment : Remove the dependency on R

[drouhling]

I need feedback on this branch which:

• replaces ball with entourages as primitive for the definition of uniformType.

• removes absRingType and uses numDomainType instead (related to Refactor norm and absolute value #4).

• instantiates the hierarchy on mathcomp's algebraic structures (see classical_sets.v and hierarchy.v).

• replaces R from standard library with any realFieldType / realType and Rbar with realFieldBar.

• moves non norm-related structures to topology.v.

Using entourages tends to lengthen proofs. In particular, I am not very satisfied with the way entourages_split replaces ball_split but I haven't found any solution yet.
In normed spaces it is less problematic since we can still use the balls defined by the norm.

This branch only use a small part of Rstruct.v, and this part does not depend on R any more. I believe this file should move to misc/, be extended with the structures from our hierarchy, and come with an example file on R containing the compatibility lemmas from Coquelicot about continuity_pt and derive_pt.

The file derive.v also takes a very long time to compile. I mean more than before. I don't know why yet. In particular Coq takes a long time to go through the proof script of diffM. I looked at the debug script for typeclasses and it seems that Coq is stuck after typeclass inference finds how to close all generated subgoals.

TODO-list:

• Generalize ereal and merge with realFieldBar (related to Merge Rbar and ereal #3).

  ereal is now generalized to any numDomainType and used everywhere. The +oo and -oo notations replace \+inf and \-inf.
  I suggest to delete Rbar.v but first we need to finish the discussion in Merge Rbar and ereal #3: does there remain any part of the arithmetic in Rbar.v we want to port to ereal ?

• Move bigmaxr theory out of Rstruct.v ? Or reimplement using bigop, generalizing and extending bigRmax theory ?

  A theory of min/max using bigop is now in hierarchy.v. This is probably not perfect and should be extended (see discussion in tentative definition of bigmaxr with bigop #114), but it is sufficient for the purpose of this PR.

• Move Rstruct.v to misc/ and extend it with our structures.

• Reintroduce commented out lemmas about R and Rbar, either translating them to realFieldType / realType / realFieldBar or putting them in an example file in misc/.

• Investigate derive.v's compilation issue.

• Clean up.

  • Be consistent with names (sometimes entourages is used, sometimes it is entourage).

  • Rework the existing documentation.

  • Rename hierarchy.v (and topology.v ?) to reflect the new organization.

  • Make sure each lemma is in the right file and no lemma has been dropped.

[affeldt-aist]

A theory of bigrmax is definitely needed (e.g., https://github.com/affeldt-aist/infotheo/blob/master/Rbigop.v). (Warning: that's old code.)

[CohenCyril]

Having a pointed type structure over something that is stable by product (and matrix) introduces a risk of inconsistency of the point operator. Indeed there would be two ways of getting it: as a pointed type of a product of as the product of two pointed type.
It would be ok to start with a realField (or realDomain? even though unnecessary), because the product of two realDomains cannot be a realDomain again.

[drouhling]

Summary of a discussion with @CohenCyril:

• I'll split this PR in two parts: one introducing the use of entourages and the other removing the dependency on standard R.
• the compilation issue in derive.v seems to be related to unification and should be fixed once Solve slowdown in derive #118 is resolved.
• some lemmas in the Bigmaxr section can be generalised and might belong to mathcomp.
• once the PRs are merged, a Rmodels directory should be created and should contain Rstruct.v, exodus.v from WIP: eudoxus reals #116 and maybe one day the model of reals using rational Cauchy filters we discussed while preparing our submission to the Coq workshop.

[CohenCyril]

@drouhling I think this issue was completely solved after the merge of #246, am I right?

[drouhling]

@drouhling I think this issue was completely solved after the merge of #246, am I right?

Indeed, this PR had no purpose any more.