[Merged by Bors] - chore: fix bug in rw? by kim-em · Pull Request #6088 · leanprover-community/mathlib4

kim-em · 2023-07-24T05:18:19Z

This fixes a problem I encountered in another tactic, where the rewrites are not being tried with the original MetavarContext.

Mathlib/Tactic/TryThis.lean

Mathlib/Tactic/Rewrites.lean

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Mathlib/Tactic/TryThis.lean

Mathlib/Tactic/Rewrites.lean

This is now [managed by the mathlib4_docs repository](https://github.com/leanprover-community/mathlib4_docs/actions), as this is required to use the new github pages deployment mechanism. The downside of this approach is that we will have to restart doc builds manually every 90 days or so.

This adds Kyle Miller's elaborators for `Type*` and `Sort*` which provide implicit universe variables. It also includes a few tests. Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Some of the tests for LibrarySearch functionality are nondetermininstic and were using `#guard_msgs` to check for specific output. This could [create spurious failures](https://github.com/leanprover-community/mathlib4/actions/runs/5810778556/job/15756601503). We switch to using `#guard_msgs (drop info)` for these tests, which still cleans up the stdout when running these tests without filtering out errors.

Add an option `lake exe graph --excludeMeta` which removes all nodes that start with `Mathlib.[Tactic|Lean|Util]`

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…d_eq_of_le_of_le_of_mul_le` earlier (#6483) This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was. Affected files: ``` Algebra.Group.UniqueProds Algebra.Order.Monoid.Basic ```

Mathlib/Tactic/Rewrites.lean

Mathlib/Tactic/TryThis.lean

Mathlib/Tactic/Rewrites.lean

thorimur · 2023-08-26T02:21:02Z

Mathlib/Tactic/Rewrites.lean

@@ -231,12 +237,13 @@ elab_rules : tactic |
      if results.isEmpty then


Github doesn't let me comment or suggest on the appropriate line, but: should we check that (reducible) rfl doesn't close the goal by itself before looking at rewrite? (Note that even rw ... at h runs rfl on the goal and can close it, so checking it is indeed applicable in every case.) For example:

example : 0 = 0 by rw? -- Try this: rw [← @Nat.le_zero] -- "no goals"

(This is technically orthogonal to this PR, and maybe should be in a different one, but was born out of thinking about computeRfl.)

Hmm... I'm not sure here. I agree the behaviour of rw? is confusing when you present it with a goal solvable by rfl, but I don't think this makes it rw?'s job to try rfl.

How about we don't modify this behaviour for now, but I'm happy to consider it separately.

Mathlib/Tactic/Rewrites.lean

kmill · 2023-08-28T13:52:44Z

The PR description doesn't seem to be accurate anymore (regarding addRewriteSuggestion). Could you fix that? Then it seems like these incremental improvements to rw? are ready to be merged.

bors d+

bors · 2023-08-28T13:52:46Z

✌️ 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.

kim-em · 2023-08-29T00:54:15Z

bors merge

This fixes a problem I encountered in another tactic, where the rewrites are not being tried with the original `MetavarContext`. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Thomas Browning <tb65536@uw.edu> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Alex J Best <alex.j.best@gmail.com> Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: michaellee94 <michael_lee1@brown.edu> Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com> Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Peiran Wu <15968905+wupr@users.noreply.github.com> Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Anne Baanen <vierkantor@vierkantor.com> Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: kkytola <kalle.kytola@aalto.fi> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: Jz Pan <acme_pjz@hotmail.com> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>

bors · 2023-08-29T02:16:34Z

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.

chore: fix bug in rw?

b8b1741

kim-em added 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 24, 2023

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 24, 2023

kim-em mentioned this pull request Jul 30, 2023

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

Closed

11 tasks

kmill reviewed Aug 1, 2023

View reviewed changes

Mathlib/Tactic/TryThis.lean Show resolved Hide resolved

Mathlib/Tactic/Rewrites.lean Show resolved Hide resolved

Mathlib/Tactic/Rewrites.lean Show resolved Hide resolved

kim-em and others added 4 commits August 2, 2023 17:56

Update Mathlib/Tactic/Rewrites.lean

df9e2f1

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Merge remote-tracking branch 'origin/master' into rw_fixes

1548d5a

tacMsg

e1a8917

suggestions from code review

08f48bf

kmill reviewed Aug 2, 2023

View reviewed changes

Mathlib/Tactic/TryThis.lean Outdated Show resolved Hide resolved

fix

4b50882

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 Aug 8, 2023

kim-em added 2 commits August 9, 2023 11:09

merge

435a434

fix merge

c67ec5d

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 9, 2023

merge

f5c3f29

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 Aug 10, 2023

thorimur reviewed Aug 10, 2023

View reviewed changes

Mathlib/Tactic/Rewrites.lean Show resolved Hide resolved

kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 10, 2023

eric-wieser and others added 8 commits August 15, 2023 19:03

feat: add Type*/Sort* and tests (#6474)

235499f

This adds Kyle Miller's elaborators for `Type*` and `Sort*` which provide implicit universe variables. It also includes a few tests. Co-authored-by: Kyle Miller <kmill31415@gmail.com>

feat(ImportGraph): add option to exclude tactics (#6153)

7c1abc3

Add an option `lake exe graph --excludeMeta` which removes all nodes that start with `Mathlib.[Tactic|Lean|Util]`

chore: isBlacklisted returns CoreM, not MetaM (#6479)

f11c793

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

chore: ForIn instance for NameMap (#6484)

4d864ef

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

chore: let Lean auto apply isBoundedDefault tactic (#6485)

60837c4

kim-em added 2 commits August 15, 2023 19:34

autoImplicit

2dffe6a

doc-string

4496b46

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 Aug 23, 2023

merge

0fdb785

kim-em requested review from alexjbest and thorimur August 24, 2023 06:49

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 Aug 24, 2023

thorimur reviewed Aug 25, 2023

View reviewed changes

Mathlib/Tactic/Rewrites.lean Outdated Show resolved Hide resolved

thorimur reviewed Aug 25, 2023

View reviewed changes

Mathlib/Tactic/TryThis.lean Outdated Show resolved Hide resolved

thorimur reviewed Aug 26, 2023

View reviewed changes

Mathlib/Tactic/Rewrites.lean Outdated Show resolved Hide resolved

thorimur reviewed Aug 26, 2023

View reviewed changes

Mathlib/Tactic/Rewrites.lean Show resolved Hide resolved

kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 27, 2023

kim-em requested review from kmill and thorimur August 27, 2023 06:30

suggestions from review

be62222

kim-em added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 28, 2023

github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 28, 2023

github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 29, 2023

bors bot changed the title ~~chore: fix bug in rw?~~ [Merged by Bors] - chore: fix bug in rw? Aug 29, 2023

bors bot closed this Aug 29, 2023

bors bot deleted the rw_fixes branch August 29, 2023 02:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: fix bug in rw?#6088

[Merged by Bors] - chore: fix bug in rw?#6088
kim-em wants to merge 118 commits intomasterfrom
rw_fixes

kim-em commented Jul 24, 2023 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur Aug 26, 2023

Uh oh!

kim-em Aug 27, 2023

Uh oh!

Uh oh!

kmill commented Aug 28, 2023

Uh oh!

bors bot commented Aug 28, 2023

Uh oh!

kim-em commented Aug 29, 2023

Uh oh!

bors bot commented Aug 29, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

		@@ -231,12 +237,13 @@ elab_rules : tactic \|
		if results.isEmpty then

Conversation

kim-em commented Jul 24, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur Aug 26, 2023

Choose a reason for hiding this comment

Uh oh!

kim-em Aug 27, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kmill commented Aug 28, 2023

Uh oh!

bors bot commented Aug 28, 2023

Uh oh!

kim-em commented Aug 29, 2023

Uh oh!

bors bot commented Aug 29, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

kim-em commented Jul 24, 2023 •

edited

Loading