Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) #15735

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) #15735

wants to merge 9 commits into from

Conversation

ericrbg
Copy link
Collaborator

@ericrbg ericrbg commented Jul 28, 2022 •
edited by github-actions bot
Loading

@ericrbg ericrbg added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands awaiting-CI The author would like to see what CI has to say before doing more work. modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. labels Jul 28, 2022
@alexjbest
Copy link
Member

alexjbest commented Jul 28, 2022 •
edited
Loading

Can you add some tests/examples?

Also why are all these tactics tagged as induction?

@TwoFX
Copy link
Member

TwoFX commented Jul 28, 2022 •
edited
Loading

How hard would it be to add a sufficesI' that also works with instances?

Since this tactic is to suffices like rintro is to intro, have you considered the name rsuffices?

PS: I have wanted this tactic to exist literally dozens of times, so thanks for adding it!

@ericrbg
Copy link
Collaborator Author

ericrbg commented Jul 28, 2022 •
edited
Loading

sufficesI should just be suffices, resetI, rotate 1 I guess? (swap is wrong here, as I found out!). I guess we could make this rsuffices/rsufficesI too, I'll try that. I'm glad I'm not the only one who's wanted this :) (ninja: it's agood idea for a second reason: it won't make the syntax highlighter misfire!)

Working on the tests Alex, and I'm not sure but I'll just leave them for consistency with obtain and maybe we should change that some other time.

@robertylewis
Copy link
Member

I also like the name rsuffices! Doesn't quite roll off the tongue, but anything to avoid more primes.

These are tagged "induction" because they're destructing terms of inductive types. All the tactic tagging is a little ad hoc and open to suggestions.

@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 28, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 28, 2022
ericrbg
ericrbg commented Jul 28, 2022
View reviewed changes
test/rcases.lean

-- This test demonstrates why `focus1` is required in the definition of `rsuffices`; otherwise
-- the `∃ ...` goal would get put _after_ the `true` goal.
example : nonempty ℕ ∧ true :=
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added some tests; this one I'm not sure what order I prefer for this specific one. This is easily decided by using/not using focus1, which feels right regardless.

@ericrbg ericrbg added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 28, 2022
@ericrbg ericrbg mentioned this pull request Jul 28, 2022
Closed
ericrbg
ericrbg commented Jul 28, 2022
View reviewed changes
test/rcases.lean Outdated Show resolved Hide resolved
@ericrbg ericrbg changed the title feat(src/tactic/rcases): suffices' = suffices + obtain feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) Jul 28, 2022
TwoFX
TwoFX reviewed Jul 29, 2022
View reviewed changes
src/tactic/rcases.lean Outdated Show resolved Hide resolved
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jul 31, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

Vierkantor
Vierkantor approved these changes Aug 19, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!

bors d+

src/tactic/rcases.lean Outdated
Comment on lines 967 to 968
-- TODO: this (I think) resets the instance cache also on the goal you need to make the instance.
-- This is not necessary; do we need this?
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's fine, resetI is already used in cases where something subtler would suffice. So I'll leave it up to you whether you want to keep this comment for future improvement.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I actually saw a case where this would be wanted, and I think that's definitely a good enough reason to keep it around. I'll remove the comments!

@bors
Copy link

bors bot commented Aug 19, 2022

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 19, 2022
@ericrbg
Copy link
Collaborator Author

ericrbg commented Aug 19, 2022

bors r+

bors bot pushed a commit that referenced this pull request Aug 19, 2022
@ericrbg
feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) (#…
34d6de4 
…15735)

Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
@bors
Copy link

bors bot commented Aug 19, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) [Merged by Bors] - feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) Aug 19, 2022
@bors bors bot closed this Aug 19, 2022
@bors bors bot deleted the ericrbg/suffices' branch August 19, 2022 16:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@ericrbg @alexjbest @TwoFX @robertylewis @mathlib-dependent-issues-bot @Vierkantor @leanprover-community-bot-assistant