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(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses #2368

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses #2368

wants to merge 9 commits into from

Conversation

semorrison
Copy link
Collaborator 

/--
Perform case analysis on a `trunc` expression, 
preferentially using the recursor `trunc.rec_on_subsingleton` 
when the goal is a subsingleton, 
and using `trunc.rec` otherwise.

Additionally, if the new hypothesis is a type class, 
reset the instance cache.
-/

@semorrison semorrison mentioned this pull request Apr 9, 2020
Closed
7 tasks
@semorrison semorrison added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Apr 9, 2020
robertylewis
robertylewis reviewed Apr 9, 2020
View reviewed changes
src/tactic/core.lean Outdated Show resolved Hide resolved
src/tactic/trunc_cases.lean Outdated Show resolved Hide resolved
src/tactic/trunc_cases.lean Outdated Show resolved Hide resolved
@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 Apr 9, 2020
@semorrison semorrison added WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 9, 2020
@semorrison
Copy link
Collaborator Author

I'm about to make this much more useful. WIP for a moment.

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Apr 10, 2020
@semorrison
Copy link
Collaborator Author

Let's try again. Here's a more powerful version.

robertylewis
robertylewis reviewed Apr 10, 2020
View reviewed changes
Copy link
Member

@robertylewis robertylewis left a comment

Choose a reason for hiding this comment

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

Okay, I think I see what's going on here a bit better. I find the logic of the script hard to parse though -- dos inside of ifs inside of dos inside of ifs inside of binds. Can this be easily refactored so that the three cases are separate methods, and trunc_cases just does the case analysis and calls the right one?

src/tactic/trunc_cases.lean Outdated Show resolved Hide resolved
src/tactic/trunc_cases.lean Outdated Show resolved Hide resolved
@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 Apr 10, 2020
@semorrison @robertylewis
Apply suggestions from code review
0d99a97 
Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>
@semorrison
Copy link
Collaborator Author

Can this be easily refactored so that the three cases are separate methods, and trunc_cases just does the case analysis and calls the right one?

Good suggestion, I'll do this tomorrow.

@semorrison semorrison 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 Apr 10, 2020
@robertylewis
Copy link
Member

Thanks, I think that's cleaner!

bors r+

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 10, 2020
@bryangingechen bryangingechen removed the awaiting-review The author would like community review of the PR label Apr 10, 2020
bors bot pushed a commit that referenced this pull request Apr 10, 2020
@semorrison
feat(tactic/trunc_cases): a tactic for case analysis on trunc hypothe…
61fa489 
…ses (#2368)

```
/--
Perform case analysis on a `trunc` expression, 
preferentially using the recursor `trunc.rec_on_subsingleton` 
when the goal is a subsingleton, 
and using `trunc.rec` otherwise.

Additionally, if the new hypothesis is a type class, 
reset the instance cache.
-/
```
@bors
Copy link

bors bot commented Apr 10, 2020

Build succeeded

@bors
Copy link

bors bot commented Apr 10, 2020

Pull request successfully merged into master.

@bors bors bot changed the title feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses [Merged by Bors] - feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses Apr 10, 2020
@bors bors bot closed this Apr 10, 2020
@bryangingechen bryangingechen deleted the trunc_cases branch April 11, 2020 01:17
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@semorrison @anrddh
feat(tactic/trunc_cases): a tactic for case analysis on trunc hypothe…
757f2e5 
…ses (leanprover-community#2368)

```
/--
Perform case analysis on a `trunc` expression, 
preferentially using the recursor `trunc.rec_on_subsingleton` 
when the goal is a subsingleton, 
and using `trunc.rec` otherwise.

Additionally, if the new hypothesis is a type class, 
reset the instance cache.
-/
```
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020
@semorrison @anrddh
feat(tactic/trunc_cases): a tactic for case analysis on trunc hypothe…
78447a4 
…ses (leanprover-community#2368)

```
/--
Perform case analysis on a `trunc` expression, 
preferentially using the recursor `trunc.rec_on_subsingleton` 
when the goal is a subsingleton, 
and using `trunc.rec` otherwise.

Additionally, if the new hypothesis is a type class, 
reset the instance cache.
-/
```
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@semorrison @cipher1024
feat(tactic/trunc_cases): a tactic for case analysis on trunc hypothe…
cf81c66 
…ses (leanprover-community#2368)

```
/--
Perform case analysis on a `trunc` expression, 
preferentially using the recursor `trunc.rec_on_subsingleton` 
when the goal is a subsingleton, 
and using `trunc.rec` otherwise.

Additionally, if the new hypothesis is a type class, 
reset the instance cache.
-/
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@robertylewis robertylewis robertylewis left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) 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
3 participants
@semorrison @robertylewis @bryangingechen