Prove 3588 !-> ... and 115 !-> ... via confluence #451
Conversation
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
|
Thanks @lyphyser! Could you please resolve merge conflicts? |
lyphyser
force-pushed
the
prove3588
branch
2 times, most recently
from
9863168 to
4dbde64
Compare
|
I have a much better version that I will push soon. |
|
OK, so the proof has been rewritten and is now much better: fast, relatively short and simple, human readable, generalizable in principle to other equations (with some work/thought needed, new issues might arise). Should be mergeable now. |
More natural since it can take any natural value, while length is > 0
This adds a bunch of lemmas in Confluence and makes two slight changes. First change is we define NF in terms of rw instead of bu, which seems more natural. It is equivalent to the other definition, which is retained as buNF, with a proof that NF <-> buNF. Second change, bu is changed to now call rw for Leaf as well. This seems more natural and is also needed to have NF <-> buNF. Note that if rw is a projection, then nothing changes, since it must be the identity on leaves.
We prove this using a proof that is specific to this equation, but designed to be mostly generalizable and perhaps possible to automatically generalize.
lyphyser
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This adds a confluence proof for 3588 !-> ..., which is interesting since it is turned by Vampire and kbcv into a system of two confluent rules, which are then implemented using Joachim Breitner's Confluence system (with some enhancements).
Not sure if it should be merged as is because it is quite slow to compile, due to the massive automated case splitting through the custom "sledgehammer" tactic that it employs (it's somewhat fine to have it alone, but if 10-100 more like this would probably be a problem).
Perhaps someone who is more experienced at Lean elaboration performance optimization can find a way to speed it up (and also automate it more ideally); otherwise it's possible that some other strategy for making confluence proofs needs to be found, or possibly a build system change where some proofs are not compiled by default.
EDIT: I rewrote the proof and now it's fast and good and all these problems are solved