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).

changed the description

changed the description

Cc @tchajed -- Perennial also contains some amount of reasoning about fractions.

I am in favor of getting rid of the coercion (which basically implies adding orders on Qp itself), but I am worried that this might be hard to port for reverse dependencies we do not control.

I think this is a great change. These coercions can be really confusing to work with.

Another thing that would be nice is if Qp had better computational behaviour. For instance if 1/2 + 1/2 was definitionally equal to 1. I'm not sure how feasible that is to implement, but not leaking the implementation in terms of Qc is definitely a requirement because Qc itself does not have nice computational behaviour.

changed the description

I think this is a great change. These coercions can be really confusing to work with.

Good to hear.

Another thing that would be nice is if Qp had better computational behaviour. For instance if 1/2 + 1/2 was definitionally equal to 1. I'm not sure how feasible that is to implement, but not leaking the implementation in terms of Qc is definitely a requirement because Qc itself does not have nice computational behaviour.

That tricky. The problem is that Qp is a Sigma type, that contains both a rational, and a proof that it's positive. However, due to opacity, the proofs in 1/2 + 1/2 and 1 will be different.

We could make these proofs transparent, but that means that 1.) we also need to make all proofs these proofs depend on transparent 2.) usually, even if you do that, computation of these proofs will be super slow.

Is there some way to at least provide a tactic for computation, even if they are not convertible? I have ended with things like assert (1/2 + 1/2 = 1)%Qp as -> and then struggled to find something to copy-paste for the proof -- I ended up with apply (bool_decide_unpack _); by compute. Something like qp_reflexivity or, even better, qp_simpl, would be great.

(But that is likely beyond the scope of this MR.)

Is there some way to at least provide a tactic for computation

apply (bool_decide_unpack _); by compute works for proving any decidable proposition, so in particular, equalities on Qp. We could have something like:

Ltac dec_solve := apply (bool_decide_unpack _); by vm_compute.

But that is likely beyond the scope of this MR.

Yes, feel free to experiment with my suggestion (you probably want to do something for error handling) and make another MR :).

I definitely support this change. Removing the coercion and avoiding using Qc would be much less confusing. We often have places where the Qc scope is needed to say something about ordering.

However, we do have a bunch of interesting Qp reasoning in Qextra.v, particularly this theorem:

Lemma Qp_split_lt (q1 q2: Qp) :
  (q1<q2)%Qc ->
  ∃ q', (q1 + q' = q2)%Qp.

I would appreciate help fixing that theorem (which I believe is the API Perennial actually needs).

mentioned in issue #84

Here's a patch for Iris https://gitlab.mpi-sws.org/iris/iris/-/tree/robbert/Qp

resolved all threads

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.

I'd say we should leave this to a possible future MR.

While we are changing the API anyway, use add/mul instead of plus/mult, to be consistent with the lemmas for nat and Z.

No strong opinion. What does the Coq stdlib use for Qc?

Also improve the Qc library in the same way.

In which way? Qc is not even our library, is it?

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.

I'd say we should leave this to a possible future MR.

OK, I agree.

While we are changing the API anyway, use add/mul instead of plus/mult, to be consistent with the lemmas for nat and Z.

No strong opinion. What does the Coq stdlib use for Qc?

nat/N/Pos and friends use add/mul/sub, while Q/Qc use plus/mult/minus.

The libraries for Q and Qc are in a pretty poor state, they are very incomplete, and do not seem to have received much maintenance though. I would thus be in favor of following the conventions in the libraries for nat/N/Pos, which are decently maintained.

Also improve the Qc library in the same way.

In which way? Qc is not even our library, is it?

Yes, it is, but since Coq's library for Qc is very incomplete, std++ provides a bunch of utilities for it. We could make those utilities consistent with those for Qp.

nat/N/Pos and friends use add/mul/sub, while Q/Qc use plus/mult/minus.

The libraries for Q and Qc are in a pretty poor state, they are very incomplete, and do not seem to have received much maintenance though. I would thus be in favor of following the conventions in the libraries for nat/N/Pos, which are decently maintained.

Seems a bit risky to diverge from the stdlib though -- after all the parts exported by stdlib will still use the other names. You can redefine them, sure, but then the lemma list is cluttered with duplicate lemmas.

Yes, it is, but since Coq's library for Qc is very incomplete, std++ provides a bunch of utilities for it. We could make those utilities consistent with those for Qp.

What would be an example for something you'd want to rename/change?

Seems a bit risky to diverge from the stdlib though -- after all the parts exported by stdlib will still use the other names. You can redefine them, sure, but then the lemma list is cluttered with duplicate lemmas.

For Qp there is not really a diverge, since it's not in the stdlib. So in that way, we can pick whatever names we want.

Also, I think we should re-implement Qc using SProp (see also #85), define Qp in terms of that. Then also for our version of Qc we can pick whatever names we want.

Also, I think we should re-implement Qc using SProp (see also #85), define Qp in terms of that. Then also for our version of Qc we can pick whatever names we want.

If that's the longer-term plan, then maybe let's wait with renaming the Qc things until we replace Qc wholesale? That will also break anyone who imports Qcanon directly (which some places do to get the notations to work).

For Qp I presume we can already establish the final names now to avoid double-rename.

If that's the longer-term plan, then maybe let's wait with renaming the Qc things until we replace Qc wholesale?

Makes sense.

For Qp I presume we can already establish the final names now to avoid double-rename.

Makes sense too.

added 12 commits

• 65702890...0ee1418d - 3 commits from branch master
• a8975c26 - Extend the theory of the positive rationals `Qp`.
• b8248336 - Rename `Qp_eq` into `Qp_to_Qc_inj_iff`.
• 979c2060 - Use `let '(...) = ...` in definitions of `Qp_le` and `Qp_lt` to avoid eager unfolding.
• 4a318aea - Define `Qp_inv`, and generalize `Qp_div` so both arguments range over `Qp`.
• efa77f8e - Add conversion function `pos_to_Qp` from `positive` to `Qp`.
• dc1960ac - Remove old comment.
• 766c2fd7 - Define `Qp` numerals in terms of `pos_to_Qp`.
• 0731b7f4 - Rename `Qp_plus` → `Qp_add`, `Qp_mult` → `Qp_mul`, and `Qp_minus` → `Qp_sub`.
• 905383de - Make `Qp` lemma names consistent with those for `Nat`, `Z` and friends.

Compare with previous version