[Merged by Bors] - refactor: define ≤/< on WithBot/WithTop by induction#19668
[Merged by Bors] - refactor: define ≤/< on WithBot/WithTop by induction#19668YaelDillies wants to merge 2 commits intomasterfrom
≤/< on WithBot/WithTop by induction#19668Conversation
PR summary f1634b790dImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
9bcb538 to
eee58b0
Compare
c55c9a0 to
d62c102
Compare
790ee1d to
54d040e
Compare
54d040e to
2a0478e
Compare
2a0478e to
3a90c63
Compare
3a90c63 to
13ecad7
Compare
13ecad7 to
dca366e
Compare
d24b33d to
0767dbb
Compare
|
This pull request has conflicts, please merge |
0767dbb to
6508514
Compare
JovanGerb
left a comment
There was a problem hiding this comment.
How does this PR interact with the recent push by @kim-em to make WithBot and WithTop be the same inductive? Given what you said in your last message, I think it would be fitting to have the ≤ relation also be a shared inductive.
I was thinking the same, in fact. It's not my favorite solution, but I'll try it |
|
I'm marking this PR as awaiting-author until you implement the shared inductive ≤ relation. Feel free to remove the label if you don't think this is a good idea anymore. |
7b40b78 to
0e9e5ab
Compare
|
Wouldn't |
MathlibTest/hint.lean
Outdated
| /-- | ||
| info: Try these: | ||
| • 🎉 finiteness | ||
| • 🎉 tauto_set |
There was a problem hiding this comment.
This looks pretty undesirable to me: the test was meant to be showing that finiteness is suggested on this goal, and now tauto_set is suggested to show finiteness of 1?
There was a problem hiding this comment.
In my opinion, hint is quite broken. It only suggests one thing and it doesn't have a way of telling which suggesting is better that which other suggestion.
There was a problem hiding this comment.
Yes, unfortunately this test is not very deterministic and so I can't do much about it
Vierkantor
left a comment
There was a problem hiding this comment.
I like the change! Now that most of the build issues and conflict with other PRs appear fixed, let's get this merged.
bors d+
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
The motivation for this change is that it is really confusing to run `intro r s shouldnthaveintroedthat` on a goal of the form `∀ r s : ℝ≥0∞, r ≤ s` and get the nonsense-looking goal `r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩` instead of an error, and similarly when destructing something of the form `∃ r s : ℝ≥0∞, r < s`. Furthermore, I suspect this improves performance.
|
Build failed: |
I suspect this improves performance
704c9d8 to
dab529e
Compare
|
bors merge |
The motivation for this change is that it is really confusing to run `intro r s shouldnthaveintroedthat` on a goal of the form `∀ r s : ℝ≥0∞, r ≤ s` and get the nonsense-looking goal `r = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩` instead of an error, and similarly when destructing something of the form `∃ r s : ℝ≥0∞, r < s`. Furthermore, I suspect this improves performance.
|
Pull request successfully merged into master. Build succeeded: |
≤/< on WithBot/WithTop by induction≤/< on WithBot/WithTop by induction
|
@YaelDillies, I'm a bit confused why you defined |
|
Indeed that was an accident. I have just opened #30848 to fix it. |
The motivation for this change is that it is really confusing to run
intro r s shouldnthaveintroedthaton a goal of the form∀ r s : ℝ≥0∞, r ≤ sand get the nonsense-looking goalr = ↑shouldnthaveintroedthat → ∃ b : α, s = ↑b ∧ shouldnthaveintroedthat ≤ b⟩instead of an error, and similarly when destructing something of the form∃ r s : ℝ≥0∞, r < s.Furthermore, I suspect this improves performance.
(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂in a dense order #20317