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

Jump to bottom

Compatible with MathComp 1.12 #275

Merged
merged 6 commits into from
Dec 21, 2020
Merged

Compatible with MathComp 1.12 #275

merged 6 commits into from
Dec 21, 2020

Conversation

pi8027
Copy link
Member

@pi8027 pi8027 commented Nov 10, 2020 •
edited
Loading

This PR makes MathComp analysis compatible with the master branch of MathComp and math-comp/real-closed#28.

CC: @affeldt-aist @mkerjean

@mkerjean
Copy link
Collaborator

This PR makes MathComp analysis compatible with the master branch of MathComp and math-comp/real-closed#28.

CC: @affeldt-aist @mkerjean

Thanks ! So inE should be replaced by in_ivt but not textually ? inE can't be adapted to include in_ivt ?

@pi8027
Copy link
Member Author

pi8027 commented Nov 10, 2020 •
edited
Loading

@mkerjean Performing rewrite inE for x \in i where i is an interval now gives us [x, x] <= i where <= is the subset relation for intervals. So we have to use in_itv instead. https://github.com/math-comp/math-comp/blob/72c13992b8961f288c412414fda206213486e25b/mathcomp/algebra/interval.v#L243

I think now you can rebase your PR #205 on top of this PR or otherwise cherry-pick my commit in your PR, to test your PR with the master branch of MathComp.

@mkerjean
Copy link
Collaborator

@mkerjean Performing rewrite inE for x \in i where i is an interval now gives us [x, x] <= i where <= is the subset relation for intervals. So we have to use in_itv instead. https://github.com/math-comp/math-comp/blob/72c13992b8961f288c412414fda206213486e25b/mathcomp/algebra/interval.v#L243

and isn't the fact that inE can't apply to intervals an issue for other developments over MathComp ? Do you think this can be corrected at the level of interval.v ?

@pi8027
Copy link
Member Author

pi8027 commented Nov 10, 2020

@mkerjean For concrete intervals whose bounds are known to be one of unbounded, open, or close, the former behavior of inE is preferable indeed. However, the new interval library (math-comp/math-comp#458) provides a way to reason about intervals abstractly. Intervals are now canonically a latticeType (if the underlying type T is a latticeType) and it allows us to reduce problems about intervals to problems about a lattice. In this case, I think that the new behavior of inE is preferable. So I would say it is not an issue we should fix on the MathComp side...

@pi8027
Copy link
Member Author

pi8027 commented Nov 10, 2020

I think @CohenCyril may have an opinion on this issue.

@CohenCyril
Copy link
Member

CohenCyril commented Nov 10, 2020 •
edited
Loading

Indeed, there seems to be a tension between generic intervals i and concrete intervals (e.g. `[a, b]), if we want inE to be readable even for abstract intervals, preferring the form `[x, x] <= i is unavoidable... however

  1. all are convertible, e.g. all of x \in `[a, b], `[x, x] <= i and a <= x <= b are convertible (you could use inE, followed by subitvE and then there are missing converibiliy lemmas between <= and in le_bound and <= in the underlying ordered Type (I suggest name leEbound) and same for <). CC @pi8027
  2. if you have an assumption of the form xab : x \in `[a, b], you should avoid using either inE or in_itv and use (itvP xab) instead.

@pi8027 pi8027 changed the title [WIP - DO NOT MERGE] compatible with MathComp master (and hopefully 1.12) Compatible with MathComp 1.12 Dec 5, 2020
@CohenCyril CohenCyril marked this pull request as ready for review December 7, 2020 10:28
@CohenCyril CohenCyril self-assigned this Dec 9, 2020
pi8027
pi8027 commented Dec 9, 2020
View reviewed changes
theories/normedtype.v
if b is BOpen_if false _ then true else false.

Lemma interval_open a b : ~~ isBClosed a -> ~~ isBClosed b ->
Lemma interval_open a b : ~~ bound_side true a -> ~~ bound_side false b ->
open [set x : R^o | x \in Interval a b].
Copy link
Member Author

Choose a reason for hiding this comment

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

@CohenCyril Thanks for fixing! Splitting Interval a b into two intervals using itv_splitI would be an easier way to prove this and interval_closed. (But we can do it later.)

Copy link
Member

Choose a reason for hiding this comment

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

Sure, I discovered a problem with the uses of eq_set here that I am a bit worried about... but, later as well...

@CohenCyril CohenCyril marked this pull request as draft December 9, 2020 01:29
@CohenCyril
Copy link
Member

I am switching this PR back to a draft to prevent untimely merges.
The reason is that I believe we should release one last version of math-comp/analysis for coq + mathcomp 1.11 with #298 before we merge this one for good.

@pi8027 pi8027 mentioned this pull request Dec 9, 2020
Merged
@CohenCyril CohenCyril marked this pull request as ready for review December 12, 2020 05:13
@affeldt-aist affeldt-aist self-requested a review December 12, 2020 05:14
@affeldt-aist
fixes
b055efe 
- fixes math-comp#277
- add the same fail-on-warnings as MathComp
- fixes math-comp#259
affeldt-aist
affeldt-aist approved these changes Dec 14, 2020
View reviewed changes
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

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

I feel that the difference between inE in in_itv for intervals is worth documenting.

@pi8027
Copy link
Member Author

pi8027 commented Dec 14, 2020

INSTALL.md has to be changed.

@affeldt-aist
remove lemmas and update INSTALL.md
33b2098 
- ltr_distW and ler_distW are now subsumed by MathComp lemmas
@pi8027
Copy link
Member Author

pi8027 commented Dec 16, 2020 •
edited
Loading

I'm fine with the changes done by Cyril and Reynald. Shall we merge? (I hope to take a look at #205 tomorrow. Merging this PR would help its process.)

@affeldt-aist affeldt-aist mentioned this pull request Dec 17, 2020
Closed
@affeldt-aist
Copy link
Member

Let's merge since it is waited for for PR #205.

@affeldt-aist affeldt-aist merged commit b96bf5a into math-comp:master Dec 21, 2020
@pi8027 pi8027 deleted the mathcomp1.12 branch January 13, 2021 13:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

@affeldt-aist affeldt-aist affeldt-aist approved these changes

Assignees

@CohenCyril CohenCyril

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@pi8027 @mkerjean @CohenCyril @affeldt-aist