Skip to content

Implement monotone partial bijections as a view

Tej Chajed requested to merge tchajed/iris-coq:view-bij into master

This is an alternative to !91 (closed), which was written prior to views. Using the view CMRA we factor the implementation into purely algebraic library and a logic-level wrapper. The logic-level wrapper exports resources which seal away the underlying ownership and has theorems which handle the ownership reasoning.

CC @dfrumin (author of !91 (closed)) and @amintimany who were using a library like this in runST and iris-logrel.

One thing I tried to do here is write the motivation for the library, as a comment in the logic-level own_bij.v library. I didn't understand the point of the library until @jung explained it to me.

Merge request reports