[Iris-Club] CMRA structure on uPred
Ralf Jung
jung at mpi-sws.org
Tue Oct 11 09:20:34 CEST 2016
Hi all,
> * valid = everything : the extension axiom does not seem to be provable
I think I actually have a counterexample, showing that it cannot be
proven. Please check carefully, I may have missed some side-condition...
As CMRA (or rather, RA), we use (option Ex {A,B})^2 -- so we have pairs
whose components are ε, A or B.
Let
P r n = r = (A,A) /\ n = 0 \/
r = (A,B) \/
r = (B,A) \/
r = (B,B)
Q1 r n = r >= (A, ε) \/ r >= (B, ε)
("Left component is not ε")
Q2 r n = r >= (ε, A) \/ r >= (ε, B)
("Right component is not ε")
These are all sufficiently closed and non-expansive and whatnot.
We have P ={0}= Q1 * Q2. So assume extension holds, then we get Q1', Q2'
such that
P = Q1' * Q2'
Q1 ={0}= Q1'
Q2 ={0}= Q2'
Now comes the contradiction:
We know that P (A,A) 1 does *not* hold, but I am going to show that
(Q1' * Q2') (A,A) 1 holds, completing the proof.
To this end, I will show (a) Q1' (A,ε) 1 and (b) Q2' (ε,A) 1.
The result follows from (A,ε) ⋅ (ε,A) = (A,A)
(a) We have P (A,B) 1, and thus Q1' r1 1 and Q2' r2 1 for some
r1 ⋅ r2 = (A,B). There are four possible decompositions:
- (ε,ε) ⋅ (A,B): This would give us Q1' (ε,ε) 1, from which we
obtain (through down-close and the equality above) that
Q1 (ε,ε) 0. However, we know that's false.
- (A,B) ⋅ (ε,ε): Can be excluded for similar reasons
(the second resource must not be ε in the 2nd component).
- (ε,B) ⋅ (A,ε): Can be excluded for similar reasons
(the first resource must not be ε in the 1st component).
- (A,ε) ⋅ (ε,B): This gives us the desired Q1' (A,ε) 1
(a) We have P (B,A) 1, and thus Q1' r1 1 and Q2' r2 1 for some
r1 ⋅ r2 = (B,A). There are again four possible decompositions,
and like above we can exclude three of them. This leaves us with
(B,ε) ⋅ (ε,A) and thus Q2' (ε,A) 1.
This completes the proof.
Man, this took me way too long... I tried for more than an hour to prove
extension with various complex schemes, and then I looked for
counterexamples involving complicated step-indexed CMRAs, and they all
failed...
Kind regards,
Ralf
More information about the Iris-Club
mailing list