[Merged by Bors] - feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future #6795

kmill · 2023-08-25T22:28:45Z

Adds new syntax for sum/product big operators for ∑ x ∈ s, f x. The set s can either be a Finset or a Set with a Fintype instance, in which case it is equivalent to ∑ x ∈ s.toFinset, f x.

Also supports ∑ (x ∈ s) (y ∈ t), f x y for Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y). Note that these are not dependent products at the moment.

Adds with clauses, so for example ∑ (x ∈ Finset.range 5) (y ∈ Finset.range 5) with x < y, x * y, which inserts a Finset.filter over the domain set.

Supports pattern matching in the variable position. This is by creating an experimental version of extBinder that uses term:max instead of binderIdent.

The new ∑ x ∈ s, f x notation is used in Algebra.BigOperators.Basic for illustration, but the old ∑ x in s, f x still works for backwards compatibility.

Zulip threads here and here

kmill · 2023-08-28T21:04:24Z

Mathlib/Algebra/BigOperators/Basic.lean

+  | `(finset% $t) => precheck t
+  | _ => Elab.throwUnsupportedSyntax
+
+-- TODO: contribute this modification back to `extBinder`


The changes to the extBinder syntax are in https://github.com/leanprover/std4/pull/234/files and in the meantime it's given as new syntax as bigOpBinder here.

jcommelin · 2023-09-14T14:29:17Z

Mathlib/Algebra/BigOperators/Basic.lean

+- `∑ x ∈ s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`,
+  where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
+- `∑ x ∈ s with p x, f x` is notation for `Finset.sum (Finset.filter p s) f`.
+- `∑ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.


Is it a valid alternative to elaborate this into a nested sum? That would automatically handle the case of t depending on x, right?

The thought was that if you wanted a nested sum then ∑ (x ∈ s), ∑ (y ∈ t), f x y is available. Yaël and Bhavik were telling me about how this sort of behavior is helpful for related notations such as for expectation, so it might be worth being consistent here.

A downside though is that this PR is not supporting dependent products, i.e., you can't do ∑ (x ∈ s) (y ∈ t x), f x y, and it's not very clear to me how to support them in a low-confusion way.

YaelDillies

I really want this notation to land. I am using it all over the place in LeanAPAP. The elaborator isn't perfect yet (no dependent products, unspecified interaction between nested and filtered products...) but it would already be a great step forward.

YaelDillies · 2023-09-15T10:36:53Z

Mathlib/Algebra/BigOperators/Basic.lean

+/-- `finset% t` elaborates `t` as a `Finset`.
+If `t` is a `Set`, then inserts `Set.toFinset`.
+Does not make use of the expected type; useful for big operators over finsets.
+```
+#check finset% Finset.range 2 -- Finset Nat
+#check finset% (Set.univ : Set Bool) -- Finset Bool
+```
+-/
+elab (name := finsetStx) "finset% " t:term : term => do
+  let u ← mkFreshLevelMVar
+  let ty ← mkFreshExprMVar (mkSort (.succ u))
+  let x ← Elab.Term.elabTerm t (mkApp (.const ``Finset [u]) ty)
+  let xty ← whnfR (← inferType x)
+  if xty.isAppOfArity ``Set 1 then
+    Elab.Term.elabAppArgs (.const ``Set.toFinset [u]) #[] #[.expr x] none false false
+  else
+    return x


Shouldn't this be moved to an earlier file?

YaelDillies · 2023-09-15T10:40:56Z

Mathlib/Algebra/BigOperators/Basic.lean

  else
    let ss ← withNaryArg 3 <| delab
-    `(∏ $(.mk i):ident in $ss, $body)
+    `(∏ $(.mk i):ident ∈ $ss, $body)

 /-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether


Suggested change

/-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether

/-- Delaborator for `Finset.sum`. The `pp.piBinderTypes` option controls whether

kmill · 2023-09-18T00:16:01Z

@YaelDillies I'm not so sure about this being the sum/prod notation, but I do support having some variant notation that constructs these (dependent) products for the domain.

In #7227 I've been working on a more flexible binder notation to upgrade all notation3 binders to have pattern matching etc. (and you can define your own binders!). Part of it is that ideally sum/prod notation uses it as well for consistency, which that PR succeeds in doing.

Potentially the variant notation could be a new binder type. Just making one up quick for sake of illustration, ∑ join% (x ∈ s) (y ∈ t), f x y could work with this system.

YaelDillies · 2023-09-18T05:38:54Z

What I really care about is the \sum ... with ..., ... notation. If that makes it easier to get in, would you mind opening a PR with just this change. Then I can copy it in LeanAPAP, check it works there, and subsequently send your PR on the merge queue.

YaelDillies

I think this is great overall and deserves to be merged even if a few details still need ironing out. We need to try out the new syntaxes to eg decide what the correct behavior for nested sums is (I think the one in this PR is already correct, but who knows).

maintainer merge

github-actions · 2024-03-22T08:52:04Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

fpvandoorn · 2024-04-29T19:30:06Z

This looks very nice from a readability standpoint. Also, the reactions on Zulip are overwhelmingly positive.
Am I correct that the current status of the delaboration is only that in is replaced by ∈?

@eric-wieser still had some reservations that he was planning to share (and I do worry a bit about the "can I rewrite the _ ∈ _?"), so please do. Otherwise I'll merge this in a few days.

YaelDillies · 2024-04-29T19:36:55Z

Yes, we are still the old elaborators here: https://github.com/leanprover-community/mathlib4/pull/6795/files#diff-daef0dcb628557383518bbc8aaabe4b289271a26e17ffd78ab3c1aae7ba1d3b2R201-R215

eric-wieser · 2024-04-29T21:50:36Z

@eric-wieser still had some reservations that he was planning to share (and I do worry a bit about the "can I rewrite the _ ∈ _?"), so please do. Otherwise I'll merge this in a few days.

I've shared these in the original zulip thread.

fpvandoorn · 2024-04-30T07:48:43Z

Ah, thanks for the link.
I think we should merge this. The notation is a lot nicer, and it shouldn't be too bad for users to adapt to this.

bors d+
bors d=YaelDillies

mathlib-bors · 2024-04-30T07:48:45Z

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-bors · 2024-04-30T07:48:45Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

YaelDillies · 2024-04-30T14:00:57Z

bors merge

mathlib-bors · 2024-04-30T14:01:01Z

👎 Rejected by label

YaelDillies · 2024-04-30T14:02:26Z

bors merge

Adds new syntax for sum/product big operators for `∑ x ∈ s, f x`. The set `s` can either be a `Finset` or a `Set` with a `Fintype` instance, in which case it is equivalent to `∑ x ∈ s.toFinset, f x`. Also supports `∑ (x ∈ s) (y ∈ t), f x y` for `Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`. Note that these are not dependent products at the moment. Adds `with` clauses, so for example `∑ (x ∈ Finset.range 5) (y ∈ Finset.range 5) with x < y, x * y`, which inserts a `Finset.filter` over the domain set. Supports pattern matching in the variable position. This is by creating an experimental version of `extBinder` that uses `term:max` instead of `binderIdent`. The new `∑ x ∈ s, f x` notation is used in `Algebra.BigOperators.Basic` for illustration, but the old `∑ x in s, f x` still works for backwards compatibility. Zulip threads [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.88.91.20x.20.E2.88.88.20s.2C.20f.20x.20instead.20of.20.E2.88.91.20x.20in.20s.2C.20f.20x/near/387352818) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Destruction.20and.20big.20operators/near/387366894) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2024-04-30T15:37:11Z

Pull request successfully merged into master.

Build succeeded:

Adds new syntax for sum/product big operators for `∑ x ∈ s, f x`. The set `s` can either be a `Finset` or a `Set` with a `Fintype` instance, in which case it is equivalent to `∑ x ∈ s.toFinset, f x`. Also supports `∑ (x ∈ s) (y ∈ t), f x y` for `Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`. Note that these are not dependent products at the moment. Adds `with` clauses, so for example `∑ (x ∈ Finset.range 5) (y ∈ Finset.range 5) with x < y, x * y`, which inserts a `Finset.filter` over the domain set. Supports pattern matching in the variable position. This is by creating an experimental version of `extBinder` that uses `term:max` instead of `binderIdent`. The new `∑ x ∈ s, f x` notation is used in `Algebra.BigOperators.Basic` for illustration, but the old `∑ x in s, f x` still works for backwards compatibility. Zulip threads [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.88.91.20x.20.E2.88.88.20s.2C.20f.20x.20instead.20of.20.E2.88.91.20x.20in.20s.2C.20f.20x/near/387352818) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Destruction.20and.20big.20operators/near/387366894) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

feat: ∑ x ∈ s, f x instead of ∑ x in s, f x

bdf5cf8

kmill added the awaiting-review The author would like community review of the PR label Aug 25, 2023

kmill added 5 commits August 25, 2023 22:30

doc fix

f7f7fd4

add precheck

ed5a5e3

lint

9484f78

switch to bigOpBinder that allows destructuring

34ae6be

get cute i + j = n antidiagonal to work

14c98fc

kmill added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 26, 2023

fix multi-binder notation

aa2ecf5

kmill added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 26, 2023

kmill mentioned this pull request Aug 26, 2023

feat: change extBinder syntax to allow destructuring leanprover-community/batteries#234

Closed

kmill commented Aug 28, 2023

View reviewed changes

jcommelin reviewed Sep 14, 2023

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 14, 2023

YaelDillies reviewed Sep 15, 2023

View reviewed changes

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26

semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:11

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 24, 2023

YaelDillies mentioned this pull request Mar 22, 2024

feat: ∑ hi : i ∈ s, f i hi syntax for big operators #11563

Open

1 task

YaelDillies added 2 commits March 22, 2024 08:36

Merge remote-tracking branch 'origin/master' into kmill_bigoperator_elem

4ba6dca

move finset% elaborator earlier

fefa25b

YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Mar 22, 2024

YaelDillies added the t-meta Tactics, attributes or user commands label Mar 22, 2024

YaelDillies approved these changes Mar 22, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Mar 22, 2024

Ruben-VandeVelde changed the title ~~feat: ∑ x ∈ s, f x instead of ∑ x in s, f x~~ feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future Mar 22, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 23, 2024

Merge remote-tracking branch 'origin/master' into kmill_bigoperator_elem

9deda7e

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 22, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 30, 2024

github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Apr 30, 2024

Merge remote-tracking branch 'origin/master' into kmill_bigoperator_elem

c35072f

YaelDillies removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 30, 2024

mathlib-bors bot changed the title ~~feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future~~ [Merged by Bors] - feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future Apr 30, 2024

mathlib-bors bot closed this Apr 30, 2024

mathlib-bors bot deleted the kmill_bigoperator_elem branch April 30, 2024 15:37

YaelDillies mentioned this pull request May 29, 2024

feat: Finset builder notation #11582

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future #6795

[Merged by Bors] - feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future #6795

kmill commented Aug 25, 2023 •

edited by eric-wieser

Loading

kmill Aug 28, 2023

jcommelin Sep 14, 2023

kmill Sep 14, 2023

YaelDillies left a comment

YaelDillies Sep 15, 2023

YaelDillies Sep 15, 2023

kmill commented Sep 18, 2023

YaelDillies commented Sep 18, 2023

YaelDillies left a comment

github-actions bot commented Mar 22, 2024

fpvandoorn commented Apr 29, 2024

YaelDillies commented Apr 29, 2024

eric-wieser commented Apr 29, 2024

fpvandoorn commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

YaelDillies commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

YaelDillies commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

	/-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
	/-- Delaborator for `Finset.sum`. The `pp.piBinderTypes` option controls whether

[Merged by Bors] - feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future #6795

[Merged by Bors] - feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future #6795

Conversation

kmill commented Aug 25, 2023 • edited by eric-wieser Loading

kmill Aug 28, 2023

Choose a reason for hiding this comment

jcommelin Sep 14, 2023

Choose a reason for hiding this comment

kmill Sep 14, 2023

Choose a reason for hiding this comment

YaelDillies left a comment

Choose a reason for hiding this comment

YaelDillies Sep 15, 2023

Choose a reason for hiding this comment

YaelDillies Sep 15, 2023

Choose a reason for hiding this comment

kmill commented Sep 18, 2023

YaelDillies commented Sep 18, 2023

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented Mar 22, 2024

fpvandoorn commented Apr 29, 2024

YaelDillies commented Apr 29, 2024

eric-wieser commented Apr 29, 2024

fpvandoorn commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

YaelDillies commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

YaelDillies commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

[Merged by Bors] - feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future #6795

[Merged by Bors] - feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future #6795

kmill commented Aug 25, 2023 •

edited by eric-wieser

Loading