[Merged by Bors] - chore(Tactic/{Positivity,NormNum}): remove support for non-canonical spellings #10344
Conversation
…spellings `Mul.mul` or `Nat.mul` etc should not ever appear in a goal, so these tactics should not support them.
eric-wieser
added
WIP
Implements #1899! Co-authored-by: Mario Carneiro <di.gama@gmail.com>
leanprover-community-mathlib4-bot
added
the
merge-conflict
| section Transparency | ||
|
|
||
| example : Add.add 10 2 = 12 := by norm_num1 | ||
| example : Nat.sub 10 1 = 9 := by norm_num1 | ||
| example : Nat.mod 10 5 = 0 := by norm_num1 | ||
| example : Sub.sub 10 1 = 9 := by norm_num1 | ||
| example : Sub.sub 10 (-2) = 12 := by norm_num1 | ||
| example : Mul.mul 10 1 = 10 := by norm_num1 | ||
| example : (Div.div 10 1 : ℚ) = 10 := by norm_num1 | ||
|
|
||
| end Transparency | ||
|
|
There was a problem hiding this comment.
These were added without explanation in 60790d4#r138404530
There was a problem hiding this comment.
I have a feeling they came up during testing and they thought it'd just be easy to support them.
There was a problem hiding this comment.
It's possible that refactors elsewhere made this behavior no longer necessary
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
I wonder if some of what I'm doing in #10293 counts for this. |
eric-wieser
added
awaiting-review
t-algebra
There was a problem hiding this comment.
The fact that everything still builds after this change shows we don't need the looser matching functionality. I only added the Mod.mod and Int.emod matching to the evalIntMod functionality because I cargo-culted this together. So I am a bit hesitant of breaking usage downstream, but in summary I think this is the right way to go.
bors r+
leanprover-community-mathlib4-bot
added
ready-to-merge
Note that I left |
|
Indeed, I recall the dispute between mathlib and core lean about dividing by negative numbers :) |
…spellings (#10344) `Mul.mul` or `Nat.mul` etc should not ever appear in a goal, so there is little reason for these tactics to support them. If these are in your goal, then something has already gone wrong and `norm_num` isn't responsible for saving you; that's `simp` or `dsimp`'s job. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310344.20removing.20norm_num.20support.20for.20Nat.2Esub.2C.20Sub.2Esub.2C.20etc/near/420507739)
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…spellings (#10344) `Mul.mul` or `Nat.mul` etc should not ever appear in a goal, so there is little reason for these tactics to support them. If these are in your goal, then something has already gone wrong and `norm_num` isn't responsible for saving you; that's `simp` or `dsimp`'s job. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310344.20removing.20norm_num.20support.20for.20Nat.2Esub.2C.20Sub.2Esub.2C.20etc/near/420507739)
Mul.mulorNat.muletc should not ever appear in a goal, so there is little reason for these tactics to support them.If these are in your goal, then something has already gone wrong and
norm_numisn't responsible for saving you; that'ssimpordsimp's job.Zulip thread