Qround.v: Add more rounding functions#291
Conversation
| (** Properties about how [Qfloor] and [Qceiling] interact with [Qplus] *) | ||
|
|
||
| Lemma Qfloor_add_Z_r : forall (x:Q) (z:Z), Qfloor (x + inject_Z z) = (Qfloor x + z)%Z. |
There was a problem hiding this comment.
Note that this property (and the related properties below) are all defined at the bottom of the file so that their proofs can take advantage of Qfloor_comp and Qceiling_comp. If you'd prefer, I can rearrange these proofs, although I may need to inline some of the details of Q{floor,ceiling}_comp to accommodate this.
| now apply (Qplus_le_compat _ _ _ _ (Qle_refl x)). | ||
| Qed. | ||
|
|
||
| Lemma Qround_to_even_resp_le : forall x y, x <= y -> (Qround_to_even x <= Qround_to_even y)%Z. |
There was a problem hiding this comment.
The implementation of this proof is particularly verbose. If you have ideas on how to make this cleaner, I'd love to hear them!
|
EDIT: Never mind, this was fixed with a rebase over #290. The I think this is because the |
0284b8d to
19b9c4d
Compare
1 participant
This adds three additional rounding functions to
Qround.v(Qtruncate,Qround_away, andQround_to_even) to complement the existingQfloorandQceilingfunctions. It also proves some corresponding properties (e.g., that each function respects<=).Fixes #283.