fixes #330 (floor and ceil subsumed by MathComp) #1244
Conversation
affeldt-aist
added
the
renaming/refactoring 🔧
affeldt-aist
changed the title
|
@proux01 could you take a quick look and potentially approved? After that it would remain to see if we still need the |
for example, I'm keep |
|
The CI errors look unrelated. |
| Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. | ||
| Proof. by rewrite intrD. Qed. | ||
|
|
||
| From mathcomp Require Import archimedean. |
There was a problem hiding this comment.
Why don't you import archimedean at the beginning of the file?
There was a problem hiding this comment.
Because only the next section needs it; if at some point this section moves to mathcomp I will not forget to erase even the Require Import.
classical/mathcomp_extra.v
Outdated
| Proof. by rewrite Num.Theory.ge_floor. Qed. | ||
|
|
||
| Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x). | ||
| Proof. by rewrite -Num.Theory.floor_ge_int. Qed. |
There was a problem hiding this comment.
Importing Num.Theory after importing archimedean (equivalently, importing archimedean before importing Num.Theory) has the advantage that you can omit Num.Theory here.
There was a problem hiding this comment.
Yes of course. I'll do that asap if you want. (Note that I still need to double-check the naming before thinking of proposing to move the lemmas to MathComp proper, which might require us to wait a bit because of name clashes.)
|
perfect |
do the names look ok to you? (that's one aspect of the review and you're in a good position to judge) |
pi8027
force-pushed
the
fixes_330
branch
2 times, most recently
from
50b5fd3
to
b3c183c
Compare
classical/mathcomp_extra.v
Outdated
| Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0. | ||
| Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed. |
There was a problem hiding this comment.
The condition x <= 0 here can be generalized to x < 1. Do you really need this lemma?
There was a problem hiding this comment.
Do you really need this lemma?
At least it is used. Of course, you can inline the proof but I think that in practice it is good to have lemmas for constants for often show up like 0, even if they have short proofs; moreover they are easily named from the general case. I'll look a bit more in detail though.
theories/altreals/realsum.v
Outdated
| rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. | ||
| rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 //. | ||
| by rewrite -RfloorE; apply lt_succ_Rfloor. | ||
| pose j := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE. |
There was a problem hiding this comment.
There are many occurrences of absz (Num.floor x). Did you check if Num.trunc can replace some of them or not? (That would be the case when x is positive and absz serves just as a type cast from int to nat.)
I agree, but general versions of these lemmas, like |
|
@affeldt-aist Shall we merge? Or do you want me to wait? |
Let's merge (it's pretty sure we'll come back to it because of the pending renamings and the cleanup of reals.v). Many thanks for all the input. |
Motivation for this change
fixes #330
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers