Prove that uPred is complete even if we remove the validity restriction in uPred_closed. (!99) · Merge requests · Iris / Iris

Jacques-Henri Jourdan requested to merge jh/upred_alt into master Dec 06, 2017

I already tried to prove that earlier and failed. But it turns out this is actually possible, and makes the definition of the uPred OFE much clearer.

I also added a comment explaining that.

Left to do: explain that in the doc. What is currently there is wrong for two reasons:

1- It does contain validity in uPred_closed (i.e., it needs to be updated with respect to this MR)

2- The stuff explained in the doc about the alternate definition based on SProp is completely wrong (it is just not isomorphic to uPred).

Edited Dec 06, 2017 by Jacques-Henri Jourdan

Prove that uPred is complete even if we remove the validity restriction in uPred_closed.