Skip to content

[Merged by Bors] - feat: the rw_search tactic#6120

Closed
kim-em wants to merge 40 commits intomasterfrom
rw_search
Closed

[Merged by Bors] - feat: the rw_search tactic#6120
kim-em wants to merge 40 commits intomasterfrom
rw_search

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jul 25, 2023 •
edited
Loading

Example usage:

example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search  -- Try this: rw [@List.length_append, @List.length_append, @add_rotate, Nat.two_mul]

Open in Gitpod

@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 25, 2023
@Komyyy Komyyy mentioned this pull request Jul 25, 2023
Open
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 30, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 3, 2023
@kim-em kim-em mentioned this pull request Aug 8, 2023
Closed
bors bot pushed a commit that referenced this pull request Aug 8, 2023
@kim-em
feat: Try this: for multiple rewrites (#6434)
730a984 
Splitting this off from #6120, hopefully for faster review.

I would like to upstream this file to Std, as it it used by `exact?`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 8, 2023
kim-em added a commit that referenced this pull request Aug 14, 2023
@kim-em
feat: Try this: for multiple rewrites (#6434)
fe8bb9d 
Splitting this off from #6120, hopefully for faster review.

I would like to upstream this file to Std, as it it used by `exact?`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 14, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 23, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 29, 2023

This PR/issue depends on:

Ruben-VandeVelde
Ruben-VandeVelde reviewed Aug 29, 2023
View reviewed changes
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 4, 2023
@Vierkantor Vierkantor self-assigned this Sep 11, 2023
Vierkantor
Vierkantor reviewed Sep 11, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@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.

Nice work! I'll have to delegate the MetaM part to someone else but the normal functional program looks good.

@Vierkantor Vierkantor removed their assignment Sep 11, 2023
kim-em
kim-em commented Oct 23, 2023
View reviewed changes
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 23, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 24, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 31, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 31, 2023
robertylewis
robertylewis reviewed Nov 1, 2023
View reviewed changes
Copy link
Copy Markdown
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.

This has been held up long enough. @semorrison if you're happy with the current state, let's merge and see how it does in practice.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 1, 2023

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Nov 1, 2023
alexjbest
alexjbest reviewed Nov 1, 2023
View reviewed changes
kim-em
kim-em commented Nov 1, 2023
View reviewed changes
kim-em and others added 3 commits November 1, 2023 13:04
@kim-em @alexjbest @robertylewis
Apply suggestions from code review
3350fad 
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
@kim-em
Merge branch 'rw_search' of github.com:leanprover-community/mathlib4 …
da0bb33 
…into rw_search
@kim-em
Merge remote-tracking branch 'origin/master' into rw_search
285bbf5
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Nov 1, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 1, 2023
@robertylewis
Copy link
Copy Markdown
Member

robertylewis commented Nov 1, 2023

@semorrison just to confirm, you saw the build failure in your last commit before you accepted the suggestions and merged, right?

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Nov 1, 2023

@semorrison just to confirm, you saw the build failure in your last commit before you accepted the suggestions and merged, right?

Yes. There was a build failure after I merged master, which I've fixed (changes to DiscrTree tree API).

bors bot pushed a commit that referenced this pull request Nov 1, 2023
@kim-em @digama0
feat: the rw_search tactic (#6120)
845846d 
Example usage:

```
example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search  -- Try this: rw [@List.length_append, @List.length_append, @add_rotate, Nat.two_mul]
```



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 1, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: the rw_search tactic [Merged by Bors] - feat: the rw_search tactic Nov 1, 2023
@bors bors bot closed this Nov 1, 2023
@bors bors bot deleted the rw_search branch November 1, 2023 03:58
fgdorais pushed a commit that referenced this pull request Nov 1, 2023
@kim-em @digama0 @fgdorais
feat: the rw_search tactic (#6120)
d578ef8 
Example usage:

```
example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search  -- Try this: rw [@List.length_append, @List.length_append, @add_rotate, Nat.two_mul]
```



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@alexjbest alexjbest alexjbest left review comments

@Vierkantor Vierkantor Vierkantor left review comments

@robertylewis robertylewis robertylewis left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@kmill kmill Awaiting requested review from kmill

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@kim-em @Vierkantor @digama0 @robertylewis @alexjbest @Ruben-VandeVelde