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.
- Add the orders
- Add a function
Qc_invfor the multiplicative inverse.
- Define the division function
Qp_divin terms of
Qp_inv, and generalize the second argument from
- Define a function
pos_to_Qpthat converts a
positiveinto a positive rational
- Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.
- Remove the coercion from
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_Qcto be consistent with other conversion functions in std++. Also rename the lemma
let '(..) = ...in the definitions of
Qp_ltto avoid Coq tactics (like
injection) to unfold these definitions eagerly. We already used this trick in e.g.,
gmapfor 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_Qpinstead of iterated addition. This avoids weird rewrites. For example, before
2was defined as
1 + 1, so rewriting with
1 = stuffin a goal containing
2turned 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
mult, to be consistent with the lemmas for
- Also improve the
Qclibrary 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.
- 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).