[Merged by Bors] - fix: make casesm and constructorm fail if no matches are found#1552
Closed
[Merged by Bors] - fix: make casesm and constructorm fail if no matches are found#1552
Conversation
dwrensha
commented
Jan 13, 2023
|
|
||
| instance : LawfulFunctor (Sum.{v, u} e) := by refine' { .. } <;> intros <;> casesm Sum _ _ <;> rfl | ||
| instance : LawfulFunctor (Sum.{v, u} e) := by | ||
| refine' { .. } <;> intros <;> (try casesm Sum _ _) <;> rfl |
Member
Author
There was a problem hiding this comment.
The casesm Sum _ _ succeeds on some subgoals and fails on some others, so we need to wrap it in a try.
Member
|
bors r+ |
bors bot
pushed a commit
that referenced
this pull request
Jan 17, 2023
The main thing I want to fix here is that `tauto` on master currently never fails *quickly*. E.g. this takes many seconds to fail: ```lean example (p : Prop) : p := by tauto ``` The reason is that the final step of `tauto` repeats until it sees a failure, and `constructorMatching` never fails, so we end up going until a timeout is hit. https://github.com/leanprover-community/mathlib4/blob/e78a2694fd2c5b00c16b4139f4a45faa17d2718d/Mathlib/Tactic/Tauto.lean#L150-L153 When I originally wrote this code, I had expected that `constructorMatching` would fail when it finds no match, similar to how the mathlib3 tactic `constructor_matching` fails when it finds no match. To fix the problem, this PR adds a `throwOnNoMatch` optional parameter to the `casesMatching` and `constructorMatching` functions, with default value set to `!recursive`. This means that the `casesm` and `constructorm` tactics will fail on no match, but the `casesm*` and `constructorm*` tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3. According to some [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/casesm.20.2F.20constructorm.20on.20no.20match.3A.20error.20or.20not.3F), other folks agree that the mathlib3 behavior was better. This PR also explicitly sets `(throwOnNoMatch := false)` on the other calls to `constructorMatching` and `casesMatching` in `tautoCore`, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting `(recursive := true)`, as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof of `Preorder.toCircularPreorder` gets pushed over the default `maxHeartbeats` timeout.
|
Pull request successfully merged into master. Build succeeded: |
jcommelin
pushed a commit
that referenced
this pull request
Jan 23, 2023
The main thing I want to fix here is that `tauto` on master currently never fails *quickly*. E.g. this takes many seconds to fail: ```lean example (p : Prop) : p := by tauto ``` The reason is that the final step of `tauto` repeats until it sees a failure, and `constructorMatching` never fails, so we end up going until a timeout is hit. https://github.com/leanprover-community/mathlib4/blob/e78a2694fd2c5b00c16b4139f4a45faa17d2718d/Mathlib/Tactic/Tauto.lean#L150-L153 When I originally wrote this code, I had expected that `constructorMatching` would fail when it finds no match, similar to how the mathlib3 tactic `constructor_matching` fails when it finds no match. To fix the problem, this PR adds a `throwOnNoMatch` optional parameter to the `casesMatching` and `constructorMatching` functions, with default value set to `!recursive`. This means that the `casesm` and `constructorm` tactics will fail on no match, but the `casesm*` and `constructorm*` tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3. According to some [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/casesm.20.2F.20constructorm.20on.20no.20match.3A.20error.20or.20not.3F), other folks agree that the mathlib3 behavior was better. This PR also explicitly sets `(throwOnNoMatch := false)` on the other calls to `constructorMatching` and `casesMatching` in `tautoCore`, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting `(recursive := true)`, as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof of `Preorder.toCircularPreorder` gets pushed over the default `maxHeartbeats` timeout.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
The main thing I want to fix here is that
tautoon master currently never fails quickly. E.g. this takes many seconds to fail:The reason is that the final step of
tautorepeats until it sees a failure, andconstructorMatchingnever fails, so we end up going until a timeout is hit.mathlib4/Mathlib/Tactic/Tauto.lean
Lines 150 to 153 in e78a269
When I originally wrote this code, I had expected that
constructorMatchingwould fail when it finds no match, similar to how the mathlib3 tacticconstructor_matchingfails when it finds no match.To fix the problem, this PR adds a
throwOnNoMatchoptional parameter to thecasesMatchingandconstructorMatchingfunctions, with default value set to!recursive. This means that thecasesmandconstructormtactics will fail on no match, but thecasesm*andconstructorm*tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3.According to some zulip discussion, other folks agree that the mathlib3 behavior was better.
This PR also explicitly sets
(throwOnNoMatch := false)on the other calls toconstructorMatchingandcasesMatchingintautoCore, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting(recursive := true), as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof ofPreorder.toCircularPreordergets pushed over the defaultmaxHeartbeatstimeout.