Put `iProp`/`iPreProp`-isomorphism into `own` construction
Each time we used a higher-order ghost construction, we had to fiddle with iProp_fold
/iProp_unfold
to deal with the iProp
/iPreProp
-isomorphism. This was needed because inG
applied the functor to iPreProp
instead of iProp
.
This MR changes this situation by apply the functor in inG
to iProp
. This moves the fiddling of the isomorphism from clients to the own
construction. This way, this only has to be done once, and clients never have to see iPreProp
.
For example, previously, for saved anything we had:
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPrePropO Σ)));
...
}.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
After this MR, this just becomes:
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
...
}.
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
own γ (to_agree x).
Also proofs of clients become much easier. For example, the 7 lines of horrible code to fiddle with the isomorphism in saved_anything_agree
is gone.