# Extend the theory of positive rationals `Qp`

This MR extends the theory of positive rationals `Qp`

. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals `Qc`

to obtain notions like orders.

### New features

- Add the orders
`Qc_le`

and`Qp_lt`

. - Add a function
`Qc_inv`

for the multiplicative inverse. - Define the division function
`Qp_div`

in terms of`Qp_inv`

, and generalize the second argument from`positive`

to`Qp`

. - Define a function
`pos_to_Qp`

that converts a`positive`

into a positive rational`Qp`

. - Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.

### Technical changes:

- Remove the coercion from
`Qp`

to`Qc`

. This follows our recent tradition of getting rid of coercions since they are more often confusing than useful. - Rename the conversion from
`Qp`

to`Qc`

from`Qp_car`

into`Qp_to_Qc`

to be consistent with other conversion functions in std++. Also rename the lemma`Qp_eq`

into`Qp_to_Qc_inj_iff`

. - Use
`let '(..) = ...`

in the definitions of`Qp_plus`

/`Qp_mult`

/`Qp_inv`

/`Qp_le`

/`Qp_lt`

to avoid Coq tactics (like`injection`

) to unfold these definitions eagerly. We already used this trick in e.g.,`gmap`

for the same reason. This works around the Coq issue that @simonfv ran into here. - Define the literals 1, 2, 3, 4 in terms of
`pos_to_Qp`

instead of iterated addition. This avoids weird rewrites. For example, before`2`

was defined as`1 + 1`

, so rewriting with`1 = stuff`

in a goal containing`2`

turned it into`stuff + stuff`

, which was extremely confusing.

### Things to discuss

- We could use Coq's extensible notation machinery to get proper notations for the literals. AFAIK this is only possible in Coq 8.9+, so that requires us to drop support for Coq 8.8.
**Do ▷** -
While we are changing the API anyway, use `add`

/`mul`

instead of`plus`

/`mult`

, to be consistent with the lemmas for`nat`

and`Z`

. - Also improve the
`Qc`

library in the same way.**Do ▷**

### Impact on reverse dependencies

This MR will cause some breakage for libraries that rely on the order on fractions, but in my opinion, this is for the better. I have ported some of the developments that use fractions in interesting ways, namely Iris, Iron, and LambdaRust. While stuff broke, I managed to shorten proofs significantly by making use of the new lemmas introduced in this MR. Also, after this MR, none of these developments rely on the conversion to `Qc`

anymore, showing that we indeed provide a reasonable API now.

Some stats:

- Iris: 66 insertions, 78 deletions
- LambdaRust: 32 insertions, 63 deletions
- Iron: no changes needed
- Examples: no changed needed, after removing an unused lemma
- gpfls: 8 insertions, 8 deletions

To land this MR, we should first merge iris!497 (merged).