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

make not_near_at_right/left equivalence #1445

Merged
merged 3 commits into from
Jan 13, 2025
Merged

make not_near_at_right/left equivalence #1445

merged 3 commits into from
Jan 13, 2025

Conversation

Yosuke-Ito-345
Copy link
Contributor

Motivation for this change

fixes #1273

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Reminder to reviewers

@Yosuke-Ito-345
Copy link
Contributor Author

Only "master / coq" failed.
Does this mean that v8.20 is incompatible with the master of Coq?
To settle this problem, do I have to compile the Coq source code from the master branch?

@affeldt-aist
Copy link
Member

I don't think you need to take any particular action. This is likely to be a temporary situation.

@Yosuke-Ito-345
Copy link
Contributor Author

@affeldt-aist
Thank you for the comment.
I am relieved to hear that!

@affeldt-aist affeldt-aist self-requested a review January 7, 2025 03:47
affeldt-aist
affeldt-aist approved these changes Jan 7, 2025
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.

It looks good enough to me. (Though it still feels like lemmas about at_right and at_left could be streamlined a bit more but I do not see how right away.)

@Yosuke-Ito-345
Copy link
Contributor Author

@affeldt-aist
Thank you for the review.
I still consider that the proof would be simpler if we assumed Variable R to be realDomainType rather than numFieldType...
(Actually I gave up that option since I could not get a reply from Cyril Cohen.)

@affeldt-aist
Copy link
Member

I still consider that the proof would be simpler if we assumed Variable R to be realDomainType rather than numFieldType...

Do you think it would be more useful with realDomainType?
We should maybe add a comment to the code to record your observation anyway.

@Yosuke-Ito-345
Copy link
Contributor Author

Yes, I think realDomainType would be useful, but only when it is also a filtered type (if I understand correctly).
However, I don't know how difficult it is to make realDomainType also filtered, so I am not confident whether we can get enough benefit from this change.

@affeldt-aist
Copy link
Member

affeldt-aist commented Jan 13, 2025 •
edited
Loading

The last commit records your observation as a comment in the code.

@Yosuke-Ito-345
Copy link
Contributor Author

@affeldt-aist
Thank you for the comment of my observation!

@Yosuke-Ito-345
Copy link
Contributor Author

Sorry, I mistakenly closed the pull request.
I have reopened it.

@affeldt-aist affeldt-aist merged commit 3cff9bb into math-comp:master Jan 13, 2025
62 of 64 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Should we make not_near_at_rightP an equivalence?
2 participants
@Yosuke-Ito-345 @affeldt-aist