[Iris-Club] CMRA structure on uPred
Jacques-Henri Jourdan
jacques-henri.jourdan at normalesup.org
Thu Sep 29 19:15:43 CEST 2016
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
>
More information about the Iris-Club
mailing list