Saved predicates

As we discussed in the chat I have created a merge request for saved predicates that we use in the runST work.

changed the description

By analogy to saved_prop.v it makes sense to have saved predicates too.

@jung @jjourdan do you agree?

Is there a way to unify the two? The construction is fundamentally the same.

I am imagining a saved_something that takes a functor as an argument, and then something like Notation saved_prop := (saved_something idRF) and Notation saved_pred T := (saved_soething funRF (const T) id).

You can, but that's only useful as an internal thing. I doubt it will work usability-wise since Coq will have a very hard time figuring out what's the functor you are using (unless you specify it), i.e. I don't know how to make type classes or canonical structures smart enough to infer it.

The type is usually given explicitly, isn't it? Like for gmaps, there's trouble with type inference, but once the type is given, all should be fine.

It means that any occurrence of saved_pred_own should be equipped with the functor. How's that the same as what happens for gmaps?

changed milestone to %Iris 3.1

Actually, saved_prop already is generic, but not generic enough: It fixes the position of the ▶.

(Btw, when pushing to the iris repository, could you please call your branch "NAME/FEATURE"? We have so many branches, things should get a little more organized.)

See my alternative proposal at https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/76.

(Btw, when pushing to the iris repository, could you please call your branch "NAME/FEATURE"? We have so many branches, things should get a little more organized.)

Oh, sorry!

mentioned in merge request !76 (merged)

Btw, I do not really like much this proposal, because it appears that we sometimes want to have something like "seved guarded predicates".

For example, in the context of iGPS, we want to store iGPS properties, i.e., Iris predicates over views that are guarded by a monotonicity property.

Of course, one could project the guard out and store the predicate only, and then remember the monotonicity condition together with the agree assertion. But this is less convenient.

I don't entirely understand your "guarded" terminology here. Do you just mean that monotone functions also form a bifunctor, and hence we can have "saved monotone predicates", and hence this MR is not general enough? Then I agree -- it seems arbitrary to single out propositions and predicates, when Iris can handle anything (as long as there is a later somewhere).

So, !76 (merged) should suit your needs then, @jjourdan?

Exactly. And indeed, !76 (merged) solves this issue.

@amintimany do you agree with closing this in favor of !76 (merged)?

@jung Yes, I agree with closing this. But I have to see if I can use !76 (merged) directly to get what I want done in for the ST project.

I agree too, but as discussed in !76 (merged), it would be good to provide instances of the generalized construction for the simple cases: plain saved propositions and plain saved predicates. That will make it easier to work with them, and then !76 (merged) really subsumes this MR.

Absolutely. Let's discuss there.

closed