-
Notifications
You must be signed in to change notification settings - Fork 299
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
[Merged by Bors] - refactor(order/lattice): adjust proofs to avoid choice #2666
Conversation
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.
LGTM
bors r+
Oh wait, I misread. You wanted feedback on whether the term mode or |
I'd prefer to avoid any use of |
@robertylewis What counts as "really necessary"? Should all the |
If you want these proofs to stay intuitionistic, then I recommend adding a test running |
I think the term mode proof in |
@urkud Is there a way to have Lean throw an error (so that CI will actually fail) if |
@b-mehta I think this is ready to go unless you want to add tests. I'll leave that up to you. |
✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
For foundational category theoretic reasons, I'd like these lattice properties to avoid choice. In particular, I'd like the proof here: #2665 to be intuitionistic. For most of them it was very easy, eg changing `finish` to `simp`. For `sup_assoc` and `inf_assoc` it's a bit more complex though - for `inf_assoc` I wrote out a term mode proof, and for `sup_assoc` I used `ifinish`. I realise `ifinish` is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.
Pull request successfully merged into master. Build succeeded: |
…mmunity#2666) For foundational category theoretic reasons, I'd like these lattice properties to avoid choice. In particular, I'd like the proof here: leanprover-community#2665 to be intuitionistic. For most of them it was very easy, eg changing `finish` to `simp`. For `sup_assoc` and `inf_assoc` it's a bit more complex though - for `inf_assoc` I wrote out a term mode proof, and for `sup_assoc` I used `ifinish`. I realise `ifinish` is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.
…mmunity#2666) For foundational category theoretic reasons, I'd like these lattice properties to avoid choice. In particular, I'd like the proof here: leanprover-community#2665 to be intuitionistic. For most of them it was very easy, eg changing `finish` to `simp`. For `sup_assoc` and `inf_assoc` it's a bit more complex though - for `inf_assoc` I wrote out a term mode proof, and for `sup_assoc` I used `ifinish`. I realise `ifinish` is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.
…mmunity#2666) For foundational category theoretic reasons, I'd like these lattice properties to avoid choice. In particular, I'd like the proof here: leanprover-community#2665 to be intuitionistic. For most of them it was very easy, eg changing `finish` to `simp`. For `sup_assoc` and `inf_assoc` it's a bit more complex though - for `inf_assoc` I wrote out a term mode proof, and for `sup_assoc` I used `ifinish`. I realise `ifinish` is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.
For foundational category theoretic reasons, I'd like these lattice properties to avoid choice.
In particular, I'd like the proof here: #2665 to be intuitionistic.
For most of them it was very easy, eg changing
finish
tosimp
. Forsup_assoc
andinf_assoc
it's a bit more complex though - forinf_assoc
I wrote out a term mode proof, and forsup_assoc
I usedifinish
. I realiseifinish
is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.