Simon Hudon (Nov 15 2020 at 04:59): 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?
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.
Paolo Giarrusso (Nov 15 2020 at 10:39):Or using IPM to avoid the goal in the first place.
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.
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).
Simon Hudon (Nov 15 2020 at 16:03):Thanks! Can you elaborate on IPM?
Simon Hudon (Nov 15 2020 at 16:06):ah! I just tried iCombine. That's so nice!
Ralf Jung (Nov 16 2020 at 11:53):Simon Hudon said:
Thanks! Can you elaborate on
IPM?
IPM = Iris Proof Mode
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: Sep 23 2023 at 07:01 UTC