[Iris-Club] CMRA structure on uPred

Robbert Krebbers mail at robbertkrebbers.nl
Mon Sep 26 16:46:39 CEST 2016


On 09/26/2016 02:27 PM, Robbert Krebbers wrote:
> 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?
The up closure on steps is making this difficult.

What we want to prove is the following:

   P ≡{n}≡ Q1 ★ Q2 → ∃ R1 R2,
     P ≡ R1 ★ R2 ∧ Q1 ≡{n}≡ R1 ∧ Q2 ≡{n}≡ R2

So, what to pick for R1 and R2? The obvious thing is:

   R1 n' x := if n' ≤ n then Q1 n' x else P n' x
   R2 n' x := if n' ≤ n then Q2 n' x else True

But this does not work: R2 is not upclosed w.r.t the steps. Given n1 ≤ n 
< n2, when we have R2 n2 x (i.e. True), there is no way to conclude R2 
n1 x (i.e. Q2 n1 x).

Anyone an idea whether there are better definitions for R1 and R2?




More information about the Iris-Club mailing list