Replace signed by itv #1410
Replace signed by itv #1410
Conversation
proux01
force-pushed
the
deprecate_signed
branch
4 times, most recently
from
0300603 to
89faa96
Compare
Generalized from realDomainType to numDomainType
From intervals on numDomainType to any porderType by making the semantics (from intervals of int to intervals of the considered type) parametric. Currently only instantiated for numDomainType though.
And deprecate signed.
proux01
force-pushed
the
deprecate_signed
branch
from
89faa96 to
9f4c2e5
Compare
| @@ -3,7 +3,7 @@ From HB Require Import structures. | |||
| From mathcomp Require Import ssreflect ssrfun ssrbool. | |||
| From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. | |||
| From mathcomp Require Import interval. | |||
| From mathcomp Require Import mathcomp_extra boolp signed. | |||
| From mathcomp Require Import mathcomp_extra boolp. | |||
There was a problem hiding this comment.
@proux01 you can remove the dependency in boolp.
BTW I think we should to backport this file to mathcomp asap.
Do you want someone else to do it (I or @hoheinzollern volunteer) or will you?
There was a problem hiding this comment.
(we just checked it goes all the way through in mathcomp/algebra)
There was a problem hiding this comment.
Great.
I can reopen in algebra. But I still think this requires some reviewing (for instance, we should probably do some kind of Private module from which we only import the canonical instances, rather than naming everything _subproof,...). Do we continue the review here before reopening or do I first reopen in algebra and we do the review in the new PR?
There was a problem hiding this comment.
I think we can continue the review here, which will make it easier to adapt the changes to analysis. When it's ready we can backport to analysis.
In order to generalize normed modules to pseudo-normed modules, we actually need it (cf https://github.com/CohenCyril/math-comp/tree/numext)
| @@ -98,7 +98,7 @@ Proof. | |||
| move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]]. | |||
| have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_max ltrDl orbC ltr01. | |||
| move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg. | |||
| exists (minr e1%:num e2%:num) => //. | |||
| exists (minr e1%:num e2%:num); first by apply: gt0; exact: RbaseSymbolsImpl.R. | |||
There was a problem hiding this comment.
I don't understand what's happening here... did you investigate the cause of this regression?
There was a problem hiding this comment.
Yes, that's what we discussed during some mathcomp meeting. Since we don't have a structure of porderNmodType, gt0 requires a numDomainType but the instance on min only provide a porderType (c.f. min_max_typ) and somehow we fail to reinfer a numDomainType (sorry, this was two months ago and I don't quite remember all the details out of my head, I would need a closer look to retrieve them).
There was a problem hiding this comment.
I see! Incidentally we are going to fix this problem in mathcomp https://github.com/CohenCyril/math-comp/tree/numext by creating partially ordered nmodules and zmodules...
There was a problem hiding this comment.
The conclusion of the last meeting on the topic was that I should do some bibliography on the topic to not get it wrong. Are you doing it? (to avoid duplicating the work)
There was a problem hiding this comment.
Yes, reading about ordered groups and riesz spaces
Motivation for this change
Complete the development of itv.v and use it in place of signed.v
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers