`QArith`: Add more rounding modes to complement `Qfloor` and `Qceiling`

Currently, QArith offers two ways to round Q values: Qfloor and Qceiling, which round toward negative and positive infinity, respectively. Besides these two definitions, there are other ways one could conceivably round a Q value:

• Truncation, i.e., rounding towards zero:

  Definition Qtruncate (x:Q) :=
    if Qle_bool 0 x
      then Qfloor x
      else Qceiling x.
  

  Alternatively, this could be defined as:

  Definition Qtruncate (x:Q) := let (n,d) := x in Z.quot n (Zpos d).
  

• Rounding towards the nearest integer, with ties broken away from zero:

  Definition Qround_away (x:Q) :=
    if Qle_bool 0 x
      then Qfloor (x + 0.5)
      else Qceiling (x - 0.5).
  

• Rounding towards the nearest integer, with ties broken to even:

  Definition Qround_to_even (x:Q) :=
    match Qcompare (Qminus x (inject_Z (Qfloor x))) 0.5 with
    | Lt => Qfloor x
    | Gt => Qceiling x
    | Eq => if Z.even (Qfloor x) then Qfloor x else Qceiling x
    end.
  

Would you be willing to upstream any of these definitions to QArith? My primary motivation for doing so is to have parity with all of the rounding modes defined in SMT-LIB's FloatingPoint theory. Currently, QArith has counterparts for RTN (Qfloor) and RTP (Qceiling), but not RNE (Qround_to_even), RNA (Qround_away), or RTZ (Qtruncate).

Start in theories/QArith/Qround.v, where Qfloor and Qceiling are defined, and compare the proposed Qtruncate, Qround_away, and Qround_to_even definitions with the SMT-LIB rounding modes. Determine which definitions should be upstreamed and add the corresponding QArith functionality with suitable verification before considering the issue complete.