-
Notifications
You must be signed in to change notification settings - Fork 106
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
Enlarge the prefix_refinement rule set #738
Merged
Merged
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
be4c49f
lib/monads/trace: prove more rules in Trace_Monad_Equations
corlewis f3c7218
lib/concurrency: improve style
corlewis 9fdbf73
lib/monads/trace: add a comment for the parallel command
corlewis 186eef5
lib/concurrency: reorder prefix_refinement arguments
corlewis 7a0377a
lib/concurrency: enlarge prefix_refinement rule set
corlewis dfef55f
lib/concurrency: update for changed prefix_refinement rules
corlewis File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think that's perfectly acceptable for the trace monad (not using
monad_eq
). Did you gain an impression on whether it would be feasible to updatemonad_eq
in a way that would make sense for the trace monad? It's not used that much in the main refinement proofs, so it wouldn't be big loss, but if the work sparked an insight, it'd be good to know.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it might be doable but it would be complicated.
The main issue is that for the nondet monad, equality can be nicely separated into
in_monad
style set membership and equality of the failure flag, both of which are resolved by rules we want anyway.However, the trace monad version of
in_monad
only handles completed monad results, it doesn't say anything about the trace that leads to the result or aboutFailed
orIncomplete
results. My guess is that with lemmas about those as well then we could updatemonad_eq
to work for the trace monad, but there's a good chance that that would end up being more effort than it saves.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, we should definitely defer until we know we want this then, esp since
monad_eq
is not used that often.