[Merged by Bors] - refactor(data/dfinsupp/basic): Improve definitional equalities of coercions #15521
Conversation
…rcions This means that `dfinsupp.coe_add` etc are true by definition, rather than requiring the application of `quotient.induction` first.
eric-wieser
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
|
|
||
| variable [Π i, has_zero (β i)] | ||
| variable (β) |
There was a problem hiding this comment.
You change from {} to () without opening a section/namespace. Why not merge with variables above?
There was a problem hiding this comment.
This was mostly accidental; although I find it's usually clearer to always use {} for type variables at the top of the file, as that means they never have to change if things are reordered within the file.
src/data/dfinsupp/basic.lean
Outdated
| instance : inhabited (Π₀ i, β i) := ⟨0⟩ | ||
|
|
||
| @[simp] | ||
| lemma coe_pre_mk (f : Π i, β i) (s : multiset ι) (hf) : | ||
| ⇑(⟦⟨f, s, hf⟩⟧ : Π₀ i, β i) = f := rfl | ||
| lemma coe_mk (f : Π i, β i) (s) : ⇑(⟨f, s⟩ : Π₀ i, β i) = f := rfl |
There was a problem hiding this comment.
You use mk' for the constructor name. Should the lemmas use mk' as well to avoid confusion with mk below?
There was a problem hiding this comment.
Yes, probably this should be called coe_mk'. Were there any others to rename?
There was a problem hiding this comment.
I did the rename. Probably I'll follow up at some point renaming mk to mk_on or extend_finset or something, meaning mk can claim the obvious name.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors merge (since the last change was just a lemma rename that was only present in one file) |
github-actions
bot
added
the
ready-to-merge
…rcions (#15521) This means that `dfinsupp.coe_add` etc are true by definition, rather than requiring the application of `quotient.induction` first. The key change is that the underlying function is no longer "hidden" under the quotient, as it does not need to be. One motivation for this is to make the API more similar to that of `finsupp`. This change eliminates `dfinsupp.pre`, instead using `{s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0}` directly. We no longer even need to create a `setoid` instance, since we can just use `trunc`. While adjusting some proofs in `data/finsupp/interval` to use the new definition, this ended up eliminating some decidable arguments. I don't think that is a consequence of this redefinition, and is incidental cleanup that could have been performed separately.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…rcions (#15521) This means that `dfinsupp.coe_add` etc are true by definition, rather than requiring the application of `quotient.induction` first. The key change is that the underlying function is no longer "hidden" under the quotient, as it does not need to be. One motivation for this is to make the API more similar to that of `finsupp`. This change eliminates `dfinsupp.pre`, instead using `{s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0}` directly. We no longer even need to create a `setoid` instance, since we can just use `trunc`. While adjusting some proofs in `data/finsupp/interval` to use the new definition, this ended up eliminating some decidable arguments. I don't think that is a consequence of this redefinition, and is incidental cleanup that could have been performed separately.
This means that
dfinsupp.coe_addetc are true by definition, rather than requiring the application ofquotient.inductionfirst.The key change is that the underlying function is no longer "hidden" under the quotient, as it does not need to be.
One motivation for this is to make the API more similar to that of
finsupp.This change eliminates
dfinsupp.pre, instead using{s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0}directly.We no longer even need to create a
setoidinstance, since we can just usetrunc.While adjusting some proofs in
data/finsupp/intervalto use the new definition, this ended up eliminating some decidable arguments. I don't think that is a consequence of this redefinition, and is incidental cleanup that could have been performed separately.