Stream: Coq users

Topic: Fractions in Iris


view this post on Zulip Simon Hudon (Nov 15 2020 at 04:59):

I'm using Qp for fractional permissions in Iris and I'm having a hard time proving something as simple as 1 / 2 + 1 / 2 = 1. Qp doesn't seem to be tied into ring or field and I haven't seen related tactics. Any pointers?

view this post on Zulip Paolo Giarrusso (Nov 15 2020 at 10:39):

Iris has its own Mattermost instance, but since positive rationals are not a ring (or field), I'd rather recommend using Search.

view this post on Zulip Paolo Giarrusso (Nov 15 2020 at 10:39):

Or using IPM to avoid the goal in the first place.

view this post on Zulip Paolo Giarrusso (Nov 15 2020 at 10:40):

To split ownership into 2, you can use iDestruct and iCombine, if you have the right Fractional and AsFractional instance.

view this post on Zulip Paolo Giarrusso (Nov 15 2020 at 10:42):

(you can also destruct Qp to find the contained Qc, but that doesn't seem to work very well).

view this post on Zulip Simon Hudon (Nov 15 2020 at 16:03):

Thanks! Can you elaborate on IPM?

view this post on Zulip Simon Hudon (Nov 15 2020 at 16:06):

ah! I just tried iCombine. That's so nice!

view this post on Zulip Ralf Jung (Nov 16 2020 at 11:53):

Simon Hudon said:

Thanks! Can you elaborate on IPM?

IPM = Iris Proof Mode

view this post on Zulip Ralf Jung (Nov 16 2020 at 11:54):

also, you can solve such decidable goals using the following tactic: apply (bool_decide_unpack _); by compute.
(see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/83 )


Last updated: Jan 29 2023 at 01:02 UTC