add comment on dec_agree in evmap
Iet me try to fix it
Try not to repeat the mistakes I made in https://gitlab.mpi-sws.org/FP/iris-atomic/commits/failed-dec_agree ;-)
If you decide you really want to keep evmap (and I am not convinced this is worth the effort), it should be raised to a higher level of abstraction so as to not expose the usage of agree. In evmap, the type worked on by the user (the type of
m) and the type of the ghost state are the same. In lambdaRust, what worked really well for us is to use different types here, so e.g. the user would work on an
Loc -> Val, and then we
fmapthat though a function
fun (v : val) => (1%Qp, to_agree v)to get the type needed for ghost ownership.
mthen still enjoys Leibniz equality and hence is nicer to work with.
This will require quite some work, so I am not sure if that's worth it.
Thanks for the advice :), and it indeed became tricky to do now. Also, I am stuck in the middle of several proofs (
evmap.v/map_agree_eq'). Is that what FAIL means? or maybe partially because you are using Coq 8.6? (I am 8.5pl3)
I am not sure what you are asking. In the failed branch (you can look at it to see what's in there), evmap.v goes though, but the lemmas in there are too weak to support flat.v. Or rather, they become too annoying to use.
I am indeed using Coq 8.6, but that branch doesn't compile. I did not complete the port.
It turns out that I am rewriting the whole stuff now :) need a bit more time