-
Notifications
You must be signed in to change notification settings - Fork 64
minor fixes and additions to exp.v
#939
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.
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
Conversation
zstone1
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just one confusing lemma statement. If adding a x!=0 condition breaks too many things, at least making the coercion explicit will make it more readable for me.
theories/exp.v
Outdated
| Qed. | ||
|
|
||
| Lemma power_posr0 a : a `^ 0 = 1. | ||
| Lemma power_pos0 x : 0 `^ x = (x == 0)%:R. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Everything about this statement is uncomfortable. The fact that we have a theorem that explicitly relies on 0 ^ 0 behavior is awkward. And this uses the most surprising coercion, nat_of_bool. I see that this lemma gets used a bunch. But would x != 0 -> 0^x = 0 work in its place?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed, it looks a bit too ssreflectish. Changing to the format you propose reduces the size of scripts a bit (see the last commit) so if moreover the statement is more readable this is a good change.
8df3452 to
9b1885c
Compare
Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
9b1885c to
421927d
Compare
* powere_pos lemmas Co-authored-by: Alessandro Bruni <[email protected]>
* powere_pos lemmas Co-authored-by: Alessandro Bruni <[email protected]>
* powere_pos lemmas Co-authored-by: Alessandro Bruni <[email protected]>
Motivation for this change
These fixes and lemmas are used in a proof of Hoelder's inequality to be PRed soon.
@hoheinzollern
Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.