saved predicates: use ofe_fun, not ofe_mor

The only two known users of this saved predicates (iris-atomic and @amintimany) only need discrete premises for their saved predicates; this makes the API easier to use for them.

changed title from saved predicates: use ofe_fun, not ofe_mur to saved predicates: use ofe_fun, not ofe_mor

added 1 commit

• 2a1af810 - saved predicates: use ofe_fun, not ofe_mor

Compare with previous version

changed milestone to %Iris 3.1

Here's how iris-atomic would use the new API: FP/iris-atomic!6 (merged)

The idea looks good to me.

IMHO, I would not use A -c> iProp Σ, but A → iProp Σ in all lemmas/operations. The -c> is mostly an internal thing to convince Coq that there is an OFEs structure.

We are doing the same for WP, there we use -c> internally, but externally we only use →.

Notice that the following -c> are actually functors:

Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).

Unfortunately, replacing -c> by -> in saved_pred_own does not work, defining the Instance breaks. I could change it for the lemmas, but is that worth it?

I could change it for the lemmas, but is that worth it?

It is at least consistent with what's in WP, and it does not unnecessarily confuse users with weird notations.

But it would be consistent between saved_pred_own and the lemmas about it, which seems worse.

added 1 commit

• 3b0c15c3 - Use normal function arrow → for saved_pred_own.

Compare with previous version

The idea is to change saved_pred_own too, of course. That's also similar to WP, which uses the normal arrow in its definition.

I just did that, and noticed a small complication: the Contractive instance needs a type annotation. I have pushed it.

Anyway, considering the type annotation for Contractive, I am not strongly in favor of one or the other, so feel free to push with or without my commit.

I just did that, and noticed a small complication: the Contractive instance needs a type annotation. I have pushed it.

Do you think using the contractivity will still work with this type annotation? I am worried this will make it not apply.

Do you think using the contractivity will still work with this type annotation? I am worried this will make it not apply.

I do not see a problem, it appears in a premise of the underlying Proper, not the conclusion.

All right. I am going to merge this then.

mentioned in commit 672d60be

merged