-
Notifications
You must be signed in to change notification settings - Fork 37
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
MapThenSumSet and several theorems for it. #99
Conversation
Signed-off-by: Karolis Petrauskas <[email protected]>
LGTM - Anticipating more It probably makes sense to add TLAPS to our CI now that we start adding theorems. |
Thanks a lot for these theorems. In order to avoid the SANY / TLAPS issue, should we EXTEND Folds for the time being (I presume the other LOCAL INSTANCEs don't cause problems)? |
+1 for changing to |
…r ReduceSet. Signed-off-by: Karolis Petrauskas <[email protected]>
It appears that it is not enough to use If I keep
Interestingly, the obligation looks identical if I keep the |
Maybe it would be better first to set up the rolling updates for TLAPS before integrating it here. |
Is it OK to merge, or should it wait for TLAPM changes? I guess that will take a long time, because the existing branches should be merged before adding more changes. |
I support merging. |
|
FiniteSetsExt!MapThenSumSet including and support TLAPS theorems. [Feature] Signed-off-by: Karolis Petrauskas <[email protected]>
Taken care of by adjusting the line numbers in |
I introduced
MapThenSumSet
operator. It was useful for me to define decreasing sequences to prove termination.Then, I proved several theorems about it. The theorems are not general enough to port them to the
Fold
operator, but maybe that's still useful.I have checked the proofs with TLAPS from PR tlaplus/tlapm#93.
The SANY parser says there is an error, but the TLAPS says OK on line 328 in
modules/FiniteSetsExt_theorems_proofs.tla
. I made a smaller case showing the same error. Documented it in tlaplus/tlapm#119.