[Iris-Club] CMRA structure on uPred

[Robbert Krebbers]

Hi all,

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

Robbert

On 09/26/2016 02:27 PM, Robbert Krebbers wrote:
> 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