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: rify tactic #7990

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: rify tactic #7990

wants to merge 13 commits into from

Conversation

PatrickMassot
Copy link
Member

Open in Gitpod

@PatrickMassot PatrickMassot added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Oct 27, 2023
j-loreaux
j-loreaux reviewed Oct 27, 2023
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

seems okay to have around, but later we should revisit for improvements.

Mathlib/Tactic/Rify.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Rify.lean Outdated Show resolved Hide resolved
timotree3
timotree3 reviewed Oct 27, 2023
View reviewed changes
Mathlib/Tactic/Rify.lean Outdated Show resolved Hide resolved
kmill
kmill reviewed Nov 18, 2023
View reviewed changes
Copy link
Contributor

@kmill kmill left a comment

Choose a reason for hiding this comment

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

Let's merge master and see if it still builds, and then I don't see why not merge it.

bors d+

Mathlib/Tactic/Attr/Register.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Zify.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Zify.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Nov 18, 2023

✌️ PatrickMassot 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-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Nov 18, 2023
@PatrickMassot
Copy link
Member Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 18, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 18, 2023
@PatrickMassot
feat: rify tactic (#7990)
f32d767
@mathlib-bors
Copy link

mathlib-bors bot commented Nov 18, 2023

Build failed:

  • Build

@Ruben-VandeVelde Ruben-VandeVelde removed the ready-to-merge This PR has been sent to bors. label Dec 4, 2023
Ruben-VandeVelde
Ruben-VandeVelde reviewed Dec 4, 2023
View reviewed changes
Mathlib/Tactic/Zify.lean
Comment on lines +103 to +116
-- `Nat.cast_sub` is already tagged as `norm_cast` but it does allow to use assumptions like
-- `m < n` or more generally `m + k ≤ n`. We add two lemmas to increase the probability that
-- `zify` will push through `ℕ` subtraction.

variable {R : Type*} [AddGroupWithOne R]

@[norm_cast] theorem Nat.cast_sub_of_add_le {m n k} (h : m + k ≤ n) :
((n - m : ℕ) : R) = n - m := Nat.cast_sub (m.le_add_right k |>.trans h)

@[norm_cast] theorem Nat.cast_sub_of_lt {m n} (h : m < n) :
((n - m : ℕ) : R) = n - m := Nat.cast_sub h.le
Copy link
Collaborator

Choose a reason for hiding this comment

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

Seems like this doesn't compile:

Error: ./././Mathlib/Tactic/Zify.lean:108:22: error: unknown identifier 'AddGroupWithOne'
Error: ./././Mathlib/Tactic/Zify.lean:111:19: error: unknown identifier 'R'
Error: ./././Mathlib/Tactic/Zify.lean:111:14: error: unknown identifier 'ℕ'
Error: ./././Mathlib/Tactic/Zify.lean:111:33: error: unknown constant 'Nat.cast_sub'
Error: ./././Mathlib/Tactic/Zify.lean:114:19: error: unknown identifier 'R'
Error: ./././Mathlib/Tactic/Zify.lean:114:14: error: unknown identifier 'ℕ'
Error: ./././Mathlib/Tactic/Zify.lean:114:33: error: unknown constant 'Nat.cast_sub'

@PatrickMassot
Copy link
Member Author

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Dec 4, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 4, 2023
@PatrickMassot
feat: rify tactic (#7990)
31d8db6
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 4, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: rify tactic [Merged by Bors] - feat: rify tactic Dec 4, 2023
@mathlib-bors mathlib-bors bot closed this Dec 4, 2023
@mathlib-bors mathlib-bors bot deleted the pm_rify branch December 4, 2023 17:17
awueth pushed a commit that referenced this pull request Dec 19, 2023
@PatrickMassot @awueth
feat: rify tactic (#7990)
9a83910
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@timotree3 timotree3 timotree3 left review comments

@j-loreaux j-loreaux j-loreaux left review comments

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

Assignees
No one assigned
Labels
delegated 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.

None yet
7 participants
@PatrickMassot @kmill @eric-wieser @timotree3 @j-loreaux @Ruben-VandeVelde @leanprover-community-mathlib4-bot