[Iris-Club] Questions on proof rules

[Ralf Jung]

Hi Jeehoon,

> I have several questions on the proof rules in the Iris 2.0 documentation.
> 
> - (Section 5.3) in the rule for deriving timeless(V(a)), I think the
> premise is not sufficient (a is a discrete COFE element).  I think we
> need more information on V to derive the conclusion..  May I ask how do
> you prove the soundness of this rule?

There is indeed a typo here. The premise should read "a is an element of
a discrete CMRA". This is defined, in the beginning of the document, to
be a CMRA where (among other properties) V ignores the step-index. (We
don't have a notion of a "discrete CMRA element". That's mostly because
we had no need for it...)

Good catch!

Notice that there was another slight mismatch here:  Namely, the way we
defined "V" on paper, it can only be passed elements of the CMRA M that
the logic is reasoning about (i.e., the CMRA M which is the domain of
ghost ownership).  However, the validity assertion is not tied to that
CMRA, you can assert validity of an element of any CMRA (at the current
step-index).  I tried to fix this now.

> - (Section 5.3) I think in general P * Q |- P /\ Q holds from the
> model.  If so, the following rules for the always modality seems redundant:
>     + always(P * Q) |- always(P /\ Q)
>     + always(P) * Q |- always(P) /\ Q
>   How do you consider this argument?

Right, I just switched the sides here. ;)
The interesting property is that we have the converse of these laws.

> - (Section 7.1) I think there is a typo in the 3rd rule: should it be on
> the universal quantification?

*lol* yeah, true ;)

> - (Section 7.1) I am not sure how to derive the 4th rule from the rules
> in Section 5..

left-to-right:

   always(P * Q)
=> always(P /\ Q)
=> always(P) /\ always(Q)
=> always(P) * always(Q)

Right-to-left:

   always(P) * always(Q)
=> always(P) /\ always(Q)
=> always(P /\ Q)
=> always(P * Q)

I've been using the converses of the rules you mentioned in the previous
section, which is probably why you were confused. I uploaded a fixed
appendix. (I now have a little script for compiling and uploading this,
since I was just doing this manually too often. ;)

> PS. I want to say thank you all for all the answers you all have
> replied.  I just didn't have a chance to say that because I did not want
> to send too much email :-)

Sure! I am really sorry here for the amount of bugs you are finding,
this is getting embarrassing... my only excuse is that I put together
the entire thing in like two days.  But I should have been more careful.

Kind regards,
Ralf