[Iris-Club] Questions on proof rules

[Jeehoon Kang]

Dear Iris Club,


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?

- (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?

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

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


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 :-)

Best,
Jeehoon

-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160823/6f04a333/attachment.html>