Skip to content

Put `iProp`/`iPreProp`-isomorphism into `own` construction

Robbert Krebbers requested to merge robbert/hide_ipreprop into master

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.

Edited by Robbert Krebbers

Merge request reports