[Merged by Bors] - feat(Data/Finsupp): add notation by eric-wieser · Pull Request #6367 · leanprover-community/mathlib4

eric-wieser · 2023-08-04T15:05:40Z

This PR provides fun₀ | 3 => a | 7 => b notation for Finsupp, which desugars to Finsupp.update and Finsupp.single, in the same way that {a, b} desugars to insert and singleton.

It also provides a matching delaborator: as an example of the effect of this, Finsupp.single_add now shows as:

Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) :
  (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂

Finally, it provides a Repr instance; though this is somewhat misleading as the syntax that is produced by Repr isn't actually computable so can't round-trip!

Discussed on Zulip here.

A nice example of the Repr in action is

#eval Finsupp.antidiagonal ⟨{1, 2}, fun x : Fin 3 => x, sorry⟩
/-
{(0, fun₀ | 1 => 1 | 2 => 2),
 (fun₀ | 1 => 1, fun₀ | 2 => 2),
 (fun₀ | 2 => 1, fun₀ | 1 => 1 | 2 => 1),
 (fun₀ | 1 => 1 | 2 => 1, fun₀ | 2 => 1),
 (fun₀ | 2 => 2, fun₀ | 1 => 1),
 (fun₀ | 1 => 1 | 2 => 2, 0)}
-/

thorimur · 2023-08-10T09:39:40Z

I really like this! :) Given that ↦ is standard for fun expressions in mathlib, though, I would suggest that:

both => and ↦ should be available as input notation, and
the delaborator and Repr instance should use ↦

so that it's as close as possible to fun syntax.

eric-wieser · 2023-08-10T10:17:10Z

both => and ↦ should be available as input notation, and

This does not work for regular functions, so I think supporting it here would just be confusing

#check show ℕ → ℕ from fun | 0 => 0 | Nat.succ n => n + 2 -- ok
#check show ℕ → ℕ from fun | 0 ↦ 0 | Nat.succ n ↦ n + 2 -- fail

If we fix fun then fun₀ will start working automatically

the delaborator and Repr instance should use ↦

Not without 1. they shouldn't!

kim-em · 2023-08-27T01:15:31Z

Mathlib/Data/Finsupp/Notation.lean

+  | _ => throw ()
+
+/-- Display `Finsupp` using `fun₀` notation. -/
+unsafe instance {α β} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β) where


Better to use Std.Util.TermUnsafe here, rather than propagating the unsafe, I think.

Couldn't you argue that Quot.unquot should be made into a safe wrapper for the same reason?

Oh, BTW there is another trick you can use here: although alpha might not be ordered, Format is, so you could just format them first and then sort the results to make the output order independent.

I decided not to do that for the same reason that the multiset repr doesn't; it gives stupid {1, 10, 11, 2, 3} orderings. I have an open issue about doing a better job of this somewhere

@digama0

This reverts commit 460c7a0. @digama0 [said](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Should.20we.20merge.20.60Quotient.2Eout.60.20and.20.60Quotient.2Eunquot.60.3F/near/388548037): > yes, the instance needs to be unsafe as it is order dependent even though it has inputs that are not

kmill

I think it would be nicer to use syntax commands instead of using leading_parser directly, but we don't need to change it for trying it out in mathlib.

Note that the documentation you've put on fun₀ is just Finsupp's documentation. At some point we should have documentation on the notation that explains the notation itself.

bors r+

This PR provides `fun₀ | 3 => a | 7 => b` notation for `Finsupp`, which desugars to `Finsupp.update` and `Finsupp.single`, in the same way that `{a, b}` desugars to `insert` and `singleton`. It also provides a matching delaborator: as an example of the effect of this, `Finsupp.single_add` now shows as: ```lean Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) : (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂ ``` Finally, it provides a `Repr` instance; though this is somewhat misleading as the syntax that is produced by `Repr` isn't actually computable so can't round-trip! [Discussed on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20.60Finsupp.60/near/381919585).

bors · 2023-09-10T14:42:29Z

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

* fix-lint: (463 commits) chore: lint-style.py was calling str.replace incorrectly chore: module doc for #find_home, #minimize_imports, import early (#7095) chore: reduce imports to Data.Rat.Cast.CharZero (#7091) chore: cleanup imports of Data/Rat/Cast/Defs (#7092) chore: linarith only needs ring1 (#7090) refactor(Data/Int/Bitwise): use `<<<` and `>>>` notation (#6789) chore: delete redundant commented-out positivity test (#7085) chore: fix docstrings, names and aligns about paracompacity of emetric spaces (#7064) feat(Data/Finsupp): add notation (#6367) refactor: re-home some meta code (#6921) fix: don't use `False` as a bool, use `false` (#7059) chore: fix reference to `compactCovering` in docstring (#7065) fix: fix link in docstring of IsWellFounded (#7063) chore: tidy various files (#7041) feat: roots in an algebra (#6740) chore: revert ProofWidgets bump in #7044 and #7056 (#7069) feat: super factorial (#6768) feat(LinearAlgebra/Matrix/Trace): add Matrix.trace_diagonal (#7061) chore: complete ProofWidgets bump (#7056) feat: More `Finset.sup'` lemmas (#7021) feat: self_lt_pow (#7058) chore: move some files to `MeasureTheory/MeasurableSpace/` (#7045) chore(RingTheory/Nilpotent): untwine two universes (#7057) feat: von Neumann Mean Ergodic Theorem (#6053) feat: (sSup, Iic) and (Ici, sInf) are Galois connections (#6951) feat: derivative along a vector (#7038) feat: check for some common git problems in CI (#7043) chore: bump ProofWidgets (#7044) feat(Topology/Algebra): add `DiscreteTopology Mˣ` (#7028) chore: simplify `by rfl` (#7039) chore: tidy various files (#7035) refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' (#6783) feat: add `DiscreteTopology.of_continuous_injective` (#7029) feat: restore the module docstring code snippet (#7030) feat: flesh out the API for `realPart` and `imaginaryPart` (#7023) chore: missing simps lemmas for `Multiplicative` defs (#7016) feat: characterize isLittleO on principal filters (#7008) doc: cleanup documentation on Basis.constr (#7007) feat: cleanup API around differentiable functions (#7004) feat: add Nat.digits_append_digits (#6999) feat: definition of the homology of a short complex (#6994) chore: implement porting notes about Polish spaces (#6991) feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915) feat: compute the integral of sqrt (1 - x ^ 2) (#6905) chore(*/TensorProduct): missing functorial lemmas (#6781) feat: a functor from a small category to a filtered category factors through a small filtered category (#6212) feat: expand API on locally integrable functions (#7006) chore: split Tactic.NormNum.Basic (#7002) feat: a few lemmas on continuous functions (#7005) feat: ZMod.castHom_self (#7013) ...

This PR provides `fun₀ | 3 => a | 7 => b` notation for `Finsupp`, which desugars to `Finsupp.update` and `Finsupp.single`, in the same way that `{a, b}` desugars to `insert` and `singleton`. It also provides a matching delaborator: as an example of the effect of this, `Finsupp.single_add` now shows as: ```lean Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) : (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂ ``` Finally, it provides a `Repr` instance; though this is somewhat misleading as the syntax that is produced by `Repr` isn't actually computable so can't round-trip! [Discussed on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20.60Finsupp.60/near/381919585).

This just extends the existing notation we already use for `Finsupp` (#6367). The two seem to coexist on the same notation without any issue.

feat(Data/Finsupp): add notation

e2a5419

eric-wieser added awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. RFC Request for comment labels Aug 4, 2023

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 4, 2023

eric-wieser added 2 commits August 4, 2023 16:51

fix linewrapping

cc5322c

Merge remote-tracking branch 'origin/master' into finsupp-notation

d57762f

eric-wieser removed the RFC Request for comment label Aug 11, 2023

kim-em reviewed Aug 27, 2023

View reviewed changes

kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 27, 2023

unsafe

460c7a0

eric-wieser added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 30, 2023

eric-wieser added 2 commits August 31, 2023 00:00

Merge remote-tracking branch 'origin/master' into finsupp-notation

7c5052c

eric-wieser force-pushed the finsupp-notation branch from 3554dc1 to b276d91 Compare September 1, 2023 15:33

kmill reviewed Sep 10, 2023

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 10, 2023

bors bot changed the title ~~feat(Data/Finsupp): add notation~~ [Merged by Bors] - feat(Data/Finsupp): add notation Sep 10, 2023

bors bot closed this Sep 10, 2023

bors bot deleted the finsupp-notation branch September 10, 2023 14:42

eric-wieser mentioned this pull request Feb 25, 2024

[Merged by Bors] - feat(Data.DFinsupp.Notation): add notation for DFinsupp #10962

Closed

callesonne pushed a commit that referenced this pull request Jun 4, 2024

feat(Data.DFinsupp.Notation): add notation for DFinsupp (#10962)

a433e64

This just extends the existing notation we already use for `Finsupp` (#6367). The two seem to coexist on the same notation without any issue.

js2357 pushed a commit that referenced this pull request Jun 18, 2024

feat(Data.DFinsupp.Notation): add notation for DFinsupp (#10962)

2a01e5e

This just extends the existing notation we already use for `Finsupp` (#6367). The two seem to coexist on the same notation without any issue.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Data/Finsupp): add notation#6367

[Merged by Bors] - feat(Data/Finsupp): add notation#6367
eric-wieser wants to merge 6 commits intomasterfrom
finsupp-notation

eric-wieser commented Aug 4, 2023 •

edited

Loading

Uh oh!

thorimur commented Aug 10, 2023 •

edited

Loading

Uh oh!

eric-wieser commented Aug 10, 2023

Uh oh!

kim-em Aug 27, 2023

Uh oh!

eric-wieser Aug 30, 2023

Uh oh!

eric-wieser Aug 31, 2023

Uh oh!

digama0 Sep 1, 2023

Uh oh!

eric-wieser Sep 1, 2023

Uh oh!

kmill left a comment

Uh oh!

bors bot commented Sep 10, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

eric-wieser commented Aug 4, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented Aug 10, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

eric-wieser commented Aug 10, 2023

Uh oh!

kim-em Aug 27, 2023

Choose a reason for hiding this comment

Uh oh!

eric-wieser Aug 30, 2023

Choose a reason for hiding this comment

Uh oh!

eric-wieser Aug 31, 2023

Choose a reason for hiding this comment

Uh oh!

digama0 Sep 1, 2023

Choose a reason for hiding this comment

Uh oh!

eric-wieser Sep 1, 2023

Choose a reason for hiding this comment

Uh oh!

kmill left a comment

Choose a reason for hiding this comment

Uh oh!

bors bot commented Sep 10, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

eric-wieser commented Aug 4, 2023 •

edited

Loading

thorimur commented Aug 10, 2023 •

edited

Loading