[Iris-Club] CMRA structure on uPred

[Robbert Krebbers]

The main purpose of defining the CMRA structure on uPred is so that I 
can define the big ops on uPred in terms of the big ops on CMRAs (see 
a4383677), and can introduce about CMRA homomorphisms to express that 
connectives commute with big ops (see 61761380).

Defining all elements to be invalid does not work. I also need the CMRA 
on uPred to have a unit (=True), and units need to be valid.

On 09/29/2016 07:15 PM, Jacques-Henri Jourdan wrote:
> 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
>>
>
>