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

lemmas about mule #403

Merged
merged 10 commits into from
Sep 18, 2021
Merged

lemmas about mule #403

merged 10 commits into from
Sep 18, 2021

Conversation

affeldt-aist
Copy link
Member

No description provided.

@affeldt-aist affeldt-aist mentioned this pull request Jul 12, 2021
Merged
@affeldt-aist affeldt-aist mentioned this pull request Jul 19, 2021
Merged
@CohenCyril
Copy link
Member

A comment about what goes wrong when unlocked?

@affeldt-aist
Copy link
Member Author

A comment about what goes wrong when unlocked?

The detail that prompted me to lock is that otherwise /= simplifies it even under bigops given difficult-to-read formulas on the screen. I guess we did not bother for other arithmetic operations so far because they are more simple.

@CohenCyril
Copy link
Member

CohenCyril commented Jul 29, 2021 •
edited
Loading

A comment about what goes wrong when unlocked?

The detail that prompted me to lock is that otherwise /= simplifies it even under bigops given difficult-to-read formulas on the screen. I guess we did not bother for other arithmetic operations so far because they are more simple.

Ok, lock is not made for that, only for kernel / unification inefficiences.
Please try nosimpl instead:

Definition mule_subdef := <the definition of multiplication>

Definition mule := nosimpl mule_subdef.

@affeldt-aist affeldt-aist changed the title a few lemmas about distributivity of \bar R lemmas about mule Jul 29, 2021
@affeldt-aist affeldt-aist added this to the 0.3.11 milestone Aug 13, 2021
proux01
proux01 approved these changes Aug 13, 2021
View reviewed changes
Copy link
Collaborator

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

Sorry for the delayed review. This looks great!
(I had some doubts at first because in floating-point arithmetic oo x 0 yields a NaN and not 0, but that's quite moral, the 0 of floats meaning "a tiny value" whereas here 0 is exactly 0)

CHANGELOG_UNRELEASED.md Outdated Show resolved Hide resolved
theories/ereal.v Outdated Show resolved Hide resolved
theories/ereal.v Outdated Show resolved Hide resolved
theories/ereal.v Outdated Show resolved Hide resolved
theories/ereal.v Outdated Show resolved Hide resolved
@proux01 proux01 mentioned this pull request Aug 13, 2021
Merged
@affeldt-aist
Copy link
Member Author

Sorry for the delayed review. This looks great!
(I had some doubts at first because in floating-point arithmetic oo x 0 yields a NaN and not 0, but that's quite moral, the 0 of floats meaning "a tiny value" whereas here 0 is exactly 0)

thank you very much, I addressed your comments, there were all to the point

proux01
proux01 approved these changes Aug 20, 2021
View reviewed changes
Copy link
Collaborator

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

I cannot assign myself nor merge but this looks mergeable to me.

@affeldt-aist affeldt-aist mentioned this pull request Aug 27, 2021
Merged
CohenCyril
CohenCyril reviewed Aug 30, 2021
View reviewed changes
theories/ereal.v Outdated Show resolved Hide resolved
CohenCyril
CohenCyril reviewed Aug 30, 2021
View reviewed changes
theories/ereal.v Outdated Show resolved Hide resolved
CohenCyril
CohenCyril reviewed Aug 30, 2021
View reviewed changes
theories/ereal.v Outdated Show resolved Hide resolved
affeldt-aist and others added 2 commits August 31, 2021 02:31
@affeldt-aist
lemmas about mule
1d9ba6a 
- distributivity lemmas
- associativity of mule
- lock definition mule with lemma muleE
@affeldt-aist @proux01
address comments
69693a3 
Co-authored-by: Pierre Roux <pierre@roux01.fr>
@affeldt-aist @CohenCyril
address comments
849bb39 
Co-authored-by: Cyril Cohen <cohen@crans.org>
@affeldt-aist
lemmas mulN1e and muleN1
5399b98 
- also fix changelog
CohenCyril
CohenCyril reviewed Sep 2, 2021
View reviewed changes
theories/ereal.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist merged commit 8dad793 into master Sep 18, 2021
@affeldt-aist affeldt-aist deleted the mule0 branch September 18, 2021 08:34
@affeldt-aist affeldt-aist mentioned this pull request Sep 19, 2021
Merged
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

@proux01 proux01 proux01 approved these changes

Assignees

@CohenCyril CohenCyril

Labels
None yet
Projects
None yet
Milestone
0.3.11
Development

Successfully merging this pull request may close these issues.
3 participants
@affeldt-aist @CohenCyril @proux01