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.
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
[Merged by Bors] - chore(PartENat): golf and improve ofNat
support
#8002
Conversation
!bench |
Here are the benchmark results for commit fb7f2f8. Benchmark Metric Change
================================================================================
+ ~Mathlib.Analysis.NormedSpace.Multilinear instructions -2.5%
+ ~Mathlib.LinearAlgebra.FreeModule.PID instructions -5.6%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions -3.4% |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
These can be inferred by `[StrictOrderedSemiring R]`.
This PR/issue depends on: |
bors d+ Pleaes merge once CI passes. Thanks, and sorry for letting this sit for a little. |
✌️ timotree3 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
!bench |
Here are the benchmark results for commit 385cee0. Benchmark Metric Change
================================================================================
+ ~Mathlib.LinearAlgebra.FreeModule.PID instructions -9.5%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions 1.9% |
This PR adds simp lemmas for `OfNat.ofNat n : PartENat`, `0 : PartENat`, and `1 : PartENat` in every place where there was a simp lemma for `((n : ℕ) : PartENat)`. This is necessary for simp confluence in the presence of lemmas such as `Nat.cast_ofNat`. In addition, instances for `CharZero` and `ZeroLEOneClass` are provided so that the lemmas from `Data/Nat/Cast/Order.lean` will apply, golfing some proofs. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
ofNat
supportofNat
support
This PR adds simp lemmas for `OfNat.ofNat n : PartENat`, `0 : PartENat`, and `1 : PartENat` in every place where there was a simp lemma for `((n : ℕ) : PartENat)`. This is necessary for simp confluence in the presence of lemmas such as `Nat.cast_ofNat`. In addition, instances for `CharZero` and `ZeroLEOneClass` are provided so that the lemmas from `Data/Nat/Cast/Order.lean` will apply, golfing some proofs. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…sts (#8006) I loogled for every occurrence of `"cast", Nat` and `"natCast"` and where the casted nat was `n`, and made sure there were corresponding `@[simp]` lemmas for `0`, `1`, and `OfNat.ofNat n`. This is necessary in general for simp confluence. Example: ```lean import Mathlib variable {α : Type*} [LinearOrderedRing α] (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo] example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp only [Nat.cast_le] -- this `@[simp]` lemma can apply example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) := by simp only [Nat.cast_ofNat] -- and so can this one example : (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp -- fails! `simp` doesn't have a lemma to bridge their results. confluence issue. ``` As far as I know, the only file this PR leaves with `ofNat` gaps is `PartENat.lean`. #8002 is addressing that file in parallel. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…sts (#8006) I loogled for every occurrence of `"cast", Nat` and `"natCast"` and where the casted nat was `n`, and made sure there were corresponding `@[simp]` lemmas for `0`, `1`, and `OfNat.ofNat n`. This is necessary in general for simp confluence. Example: ```lean import Mathlib variable {α : Type*} [LinearOrderedRing α] (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo] example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp only [Nat.cast_le] -- this `@[simp]` lemma can apply example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) := by simp only [Nat.cast_ofNat] -- and so can this one example : (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp -- fails! `simp` doesn't have a lemma to bridge their results. confluence issue. ``` As far as I know, the only file this PR leaves with `ofNat` gaps is `PartENat.lean`. #8002 is addressing that file in parallel. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…sts (#8006) I loogled for every occurrence of `"cast", Nat` and `"natCast"` and where the casted nat was `n`, and made sure there were corresponding `@[simp]` lemmas for `0`, `1`, and `OfNat.ofNat n`. This is necessary in general for simp confluence. Example: ```lean import Mathlib variable {α : Type*} [LinearOrderedRing α] (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo] example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp only [Nat.cast_le] -- this `@[simp]` lemma can apply example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) := by simp only [Nat.cast_ofNat] -- and so can this one example : (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp -- fails! `simp` doesn't have a lemma to bridge their results. confluence issue. ``` As far as I know, the only file this PR leaves with `ofNat` gaps is `PartENat.lean`. #8002 is addressing that file in parallel. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…sts (#8006) I loogled for every occurrence of `"cast", Nat` and `"natCast"` and where the casted nat was `n`, and made sure there were corresponding `@[simp]` lemmas for `0`, `1`, and `OfNat.ofNat n`. This is necessary in general for simp confluence. Example: ```lean import Mathlib variable {α : Type*} [LinearOrderedRing α] (m n : ℕ) [m.AtLeastTwo] [n.AtLeastTwo] example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp only [Nat.cast_le] -- this `@[simp]` lemma can apply example : ((OfNat.ofNat m : ℕ) : α) ≤ ((OfNat.ofNat n : ℕ) : α) ↔ (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) := by simp only [Nat.cast_ofNat] -- and so can this one example : (OfNat.ofNat m : α) ≤ (OfNat.ofNat n : α) ↔ (OfNat.ofNat m : ℕ) ≤ (OfNat.ofNat n : ℕ) := by simp -- fails! `simp` doesn't have a lemma to bridge their results. confluence issue. ``` As far as I know, the only file this PR leaves with `ofNat` gaps is `PartENat.lean`. #8002 is addressing that file in parallel. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This PR adds simp lemmas for
OfNat.ofNat n : PartENat
,0 : PartENat
, and1 : PartENat
in every place where there was a simp lemma for((n : ℕ) : PartENat)
. This is necessary for simp confluence in the presence of lemmas such asNat.cast_ofNat
. In addition, instances forCharZero
andZeroLEOneClass
are provided so that the lemmas fromData/Nat/Cast/Order.lean
will apply, golfing some proofs.[Nontrivial R]
#8129