[Iris-Club] CMRA structure on uPred

[Ralf Jung]

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