[Iris-Club] CMRA structure on uPred

[Robbert Krebbers]

Hi all,

in the attempt of refactoring some stuff related to connectives that 
commute with big ops (both those on CMRAs and those on uPred), I want to 
introduce the notion of a CMRA homomorphism:

   Class CMRAHomomorphism {A B : cmraT} (f : A → B) := {
     cmra_homomorphism_ne n :> Proper (dist n ==> dist n) f;
     cmra_homomorphism_validN n x : ✓{n} x → ✓{n} f x;
     cmra_homomorphism x y : f (x ⋅ y) ≡ f x ⋅ f y
   }.

Now, provided we would have a cmra structure on uPred, we could use the 
homomorphism class to express properties like:

          ◯ (x ⋅ y) ≡ ◯ x ⋅ ◯ y
   {[ i := x ⋅ y ]} ≡ {[ i := x ]} ⋅ {[ i := y ]}
      own γ (x ⋅ y) ≡ own γ x ★ own γ y
          ▷ (P ★ Q) ≡ ▷ P ★ ▷ Q

This way, we could generically get that the above connectives commute 
with big ops.

But how do we define the CMRA structure on uPred? My attempt is as follows:

   Instance uPred_valid' : Valid (uPred M) := λ _, True.
   Instance uPred_validN' : ValidN (uPred M) := λ _ _, True.
   Instance uPred_op : Op (uPred M) := uPred_sep.
   Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.

(Note that I op needs to be ★ and core needs to be True for the 
homomorphisms to be sensible).

Unfortunately, I am unable to prove the CMRA extension axiom. Anyone an 
idea whether this is provable at all?

Robbert