[Iris-Club] CMRA structure on uPred

[Ralf Jung]

Hi,

> it turns out that this can be made to work when defining P to be valid
> if it is logically valid, i.e.:
> 
>   Instance uPred_valid : Valid (uPred M) := λ P,
>     ∀ n x, ✓{n} x → P n x.
> 
> For the extension axiom we have to show:
> 
>   ✓{n} P → P ≡{n}≡ Q1 ★ Q2 → ∃ R1 R2,
>     P ≡ R1 ★ R2 ∧ Q1 ≡{n}≡ R1 ∧ Q2 ≡{n}≡ R2
> 
> Since we have ✓{n} P, we have P ≡{n}≡ True and Q1 ≡{n}≡ True. So, then
> we simply pick R1 := True and R2 := P. Qed.
> 
> See commit:
> 
> 
> https://gitlab.mpi-sws.org/FP/iris-coq/commit/7c762be1d2769fe486b34197ad38a3611194ea3d

Nice observation!

Of course, I had to immediately wonder whether this could be used to get
higher-order ghost state with * being composition. To this end, we would
have to show that uPred is a locally non-expansive functor from CMRA to
CMRA, right? IIRC last time we looked at this we concluded it would not
work.

The validity you picked is however not the one we would want for ghost
ownership, since we do want to talk about assertions that are not valid.
I did not expect CMRA extension to be a problem since it never was a
problem before, so I'd like to understand better what is happening here...
  I can't actually see a reason why the extension axiom should hold, but
I also cannot find a counterexample.  What the proof somehow has to do
is to "complete" the missing parts (i.e. Q1 and Q2 above step-index n)
in a "natural" way. The obvious choice is to just repeat step-index [n]
infinitely, but of course that doesn't give us anything equal to P... so
maybe Q1 repeats the step-index, and Q2 is "Q1 -* P" (i.e., "P without
Q1)? I will have to write this down on paper...

Kind regards,
Ralf