[Agda] TwoPhase refinement of TCommit in Agda : Some thoughts.

[Apostolis Xekoukoulotakis]

I am trying to use TLA from Agda. I have just managed to prove the TwoPhase
refinement of TCommit. I have some thoughts and questions about this that
relates to Agda too.
https://groups.google.com/d/msg/tlaplus/d_Mm7lYMQaI/2XdKAQpIDgAJ

The main problem is that specifications have global invariants that need to
be proven, to prove that they are a refinement of another. But then, we
lose the ability to use the restrictions of the refinement as a guide for
the definition of the refining spec.

In other words, I want to postpone the definition of the refining spec as
much as possible and introduce restrictions as soon as possible, in order
to have type-driven development.
This is not very easy with global invariants.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181214/66fa6078/attachment.html>