[Merged by Bors] - feat(Data/Finsupp): make toMultiset and antidiagonal computable #6331
Conversation
In Lean 3, the comptubility of `Finsupp.toMultiset` was poisoned by the `AddMonoid (α →₀ ℕ)` instance, even though this was not used in computation. This is no longer the case in Lean 4, so we can make this computable by adding a `DecidableEq α` argument.
eric-wieser
added
awaiting-review
eric-wieser
changed the title
….toMultiset-computable
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by ericrbg. |
| @@ -1473,6 +1474,7 @@ theorem coeff_zero_one : coeff R 0 (1 : PowerSeries R) = 1 := | |||
| theorem coeff_mul (n : ℕ) (φ ψ : PowerSeries R) : | |||
| coeff R n (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by | |||
| symm | |||
| erw [MvPowerSeries.coeff_mul] | |||
There was a problem hiding this comment.
Could you explain (in a comment?) why a normal rw doesn't work here?
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
| @@ -1473,6 +1474,7 @@ theorem coeff_zero_one : coeff R 0 (1 : PowerSeries R) = 1 := | |||
| theorem coeff_mul (n : ℕ) (φ ψ : PowerSeries R) : | |||
| coeff R n (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by | |||
| symm | |||
| erw [MvPowerSeries.coeff_mul] -- `rw` can't see that `PowerSeries = MvPowerSeries Unit` | |||
There was a problem hiding this comment.
not to be a nitpicker but in this case shouldn't we just have a lemma to this effect and normal rw it? [or does that cause motive issues]
the defeq abuse before wasn't great either though
There was a problem hiding this comment.
This lemma is the place where we're building that lemma! The problem would go away if we made PowerSeries reducible, or introduced a function to convert between it and MvPowerSeries
There was a problem hiding this comment.
I'll make a follow-up PR to golf this proof
|
bors merge |
In Lean 3, the computability of `Finsupp.toMultiset` was poisoned by the `AddMonoid (α →₀ ℕ)` instance, even though this was not used in computation. This is no longer the case in Lean 4, so we can make this computable by adding a `DecidableEq α` argument. We loosely follow the pattern used with `DFinsupp`, where we split the declaration in two, as only one direction needs `DecidableEq α`. As a result, `Finsupp.toMultiset` is now only an `AddMonoidHom`, though `Multiset.toFinset` remains an equiv. We're missing some of the formatting infrastructure for this to be pretty, but this now works: ```lean #eval ((Finsupp.mk Finset.univ ![1, 2, 3] sorry).antidiagonal).image fun x : _ × _ => (x.1.toFun, x.2.toFun) ```
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
In Lean 3, the computability of `Finsupp.toMultiset` was poisoned by the `AddMonoid (α →₀ ℕ)` instance, even though this was not used in computation. This is no longer the case in Lean 4, so we can make this computable by adding a `DecidableEq α` argument. We loosely follow the pattern used with `DFinsupp`, where we split the declaration in two, as only one direction needs `DecidableEq α`. As a result, `Finsupp.toMultiset` is now only an `AddMonoidHom`, though `Multiset.toFinset` remains an equiv. We're missing some of the formatting infrastructure for this to be pretty, but this now works: ```lean #eval ((Finsupp.mk Finset.univ ![1, 2, 3] sorry).antidiagonal).image fun x : _ × _ => (x.1.toFun, x.2.toFun) ```
In Lean 3, the computability of
Finsupp.toMultisetwas poisoned by theAddMonoid (α →₀ ℕ)instance, even though this was not used in computation. This is no longer the case in Lean 4, so we can make this computable by adding aDecidableEq αargument.We loosely follow the pattern used with
DFinsupp, where we split the declaration in two, as only one direction needsDecidableEq α. As a result,Finsupp.toMultisetis now only anAddMonoidHom, thoughMultiset.toFinsetremains an equiv.We're missing some of the formatting infrastructure for this to be pretty, but this now works: