[Iris-Club] CMRA structure on uPred

[Jacques-Henri Jourdan]

Well, but I do not really see the point of having a CMRA structure where 
the only valid element (up to equivalence) is True... You could also set 
all predicates to be invalid. It seems that this CMRA structure is here 
just for making notations nicer but does not reveal anything about the 
structure of uniform predicates.

Did I misunderstood something?

On 09/27/2016 10:37 AM, Robbert Krebbers wrote:
> 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
>