[Merged by Bors] - feat: Finset builder notation #11582

YaelDillies · 2024-03-22T12:14:57Z

Define elaborators (but no delaborators) to elaborate the following notations to a Finset:

In Data.Finset.Basic,

{x ∈ s | p x}

In Data.Fintype.Basic,

{x | p x}
{x : α | p x}
{x ∉ s | p x}
{x ≠ a | p x}

In Order.Interval.Finset.Basic,

{x ≤ a | p x}
{x ≥ a | p x}
{x < a | p x}
{x > a | p x}

The general heuristic for deciding whether to elaborate a given notation as a Set or Finset is:

Check whether the expected type is Finset ?α.
- If it is, elaborate as a Finset.
- If it isn't, check whether the expected type of s in the notation is Finset ?α.
  - If it is, elaborate as a Finset.
  - If it isn't or there is no s in the notation, elaborate as a Set.

There is currently a gotcha that elaboration to Set is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See Zulip.

Mathlib/Data/List/Pairwise.lean

Mathlib/Data/Finset/Basic.lean

Mathlib/Data/Fintype/Basic.lean

YaelDillies · 2024-05-29T12:15:44Z

The new notations here intersect a lot with the notations introduced by #6795, so I'm thinking I should be creating a new syntax category setBinder instead of reusing the existing binderPred.

github-actions · 2024-06-11T17:54:44Z

PR summary 985d7de269

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Init.Set	1	2	+1 (+100.00%)

Import changes for all files

Files	Import difference
`Mathlib.Init.Set`	1

Declarations diff

+ elabFinsetBuilderIxx
+ elabFinsetBuilderSep
+ elabFinsetBuilderSetOf
+ elabSetBuilder
+ knownToBeFinsetNotSet

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

YaelDillies · 2024-06-11T18:12:26Z

The new notations here intersect a lot with the notations introduced by #6795, so I'm thinking I should be creating a new syntax category setBinder instead of reusing the existing binderPred.

Given that this is completely orthogonal to the current PR, I will do that in a later PR.

joneugster

Thanks for the PR! Generally looks clean to me. Here are some remaining comments

Mathlib/Combinatorics/Enumerative/DoubleCounting.lean

test/finset_builder.lean

Mathlib/Data/Fintype/Basic.lean

test/finset_builder.lean

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

joneugster · 2024-08-15T13:53:06Z

maintainer merge

github-actions · 2024-08-15T13:53:17Z

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

kmill · 2024-08-15T22:24:42Z

Thanks!

bors r+

kmill · 2024-08-15T22:27:53Z

Mathlib/Data/Finset/Basic.lean

+    -- If the expected type is known to be `Set ?α`, give up. If it is not known to be `Set ?α` or
+    -- `Finset ?α`, check the expected type of `s`.
+    unless ← knownToBeFinsetNotSet expectedType? do
+      let ty ← try whnfR (← inferType (← elabTerm s none)) catch _ => throwUnsupportedSyntax


It's too bad that this elabTerm s none is wasted work. Maybe in a followup it could be saved and then inserted into the Syntax on line 2201 using exprToSyntax.

Yes, that makes sense

Define elaborators (but no delaborators) to elaborate the following notations to a `Finset`: In `Data.Finset.Basic`, * `{x ∈ s | p x}` In `Data.Fintype.Basic`, * `{x | p x}` * `{x : α | p x}` * `{x ∉ s | p x}` * `{x ≠ a | p x}` In `Order.Interval.Finset.Basic`, * `{x ≤ a | p x}` * `{x ≥ a | p x}` * `{x < a | p x}` * `{x > a | p x}` The general heuristic for deciding whether to elaborate a given notation as a `Set` or `Finset` is: * Check whether the expected type is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't, check whether the expected type of `s` in the notation is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't or there is no `s` in the notation, elaborate as a `Set`. There is currently a gotcha that elaboration to `Set` is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset).

mathlib-bors · 2024-08-15T23:53:36Z

Build failed (retrying...):

Build

Define elaborators (but no delaborators) to elaborate the following notations to a `Finset`: In `Data.Finset.Basic`, * `{x ∈ s | p x}` In `Data.Fintype.Basic`, * `{x | p x}` * `{x : α | p x}` * `{x ∉ s | p x}` * `{x ≠ a | p x}` In `Order.Interval.Finset.Basic`, * `{x ≤ a | p x}` * `{x ≥ a | p x}` * `{x < a | p x}` * `{x > a | p x}` The general heuristic for deciding whether to elaborate a given notation as a `Set` or `Finset` is: * Check whether the expected type is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't, check whether the expected type of `s` in the notation is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't or there is no `s` in the notation, elaborate as a `Set`. There is currently a gotcha that elaboration to `Set` is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset).

mathlib-bors · 2024-08-16T00:09:46Z

This PR was included in a batch that was canceled, it will be automatically retried

Define elaborators (but no delaborators) to elaborate the following notations to a `Finset`: In `Data.Finset.Basic`, * `{x ∈ s | p x}` In `Data.Fintype.Basic`, * `{x | p x}` * `{x : α | p x}` * `{x ∉ s | p x}` * `{x ≠ a | p x}` In `Order.Interval.Finset.Basic`, * `{x ≤ a | p x}` * `{x ≥ a | p x}` * `{x < a | p x}` * `{x > a | p x}` The general heuristic for deciding whether to elaborate a given notation as a `Set` or `Finset` is: * Check whether the expected type is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't, check whether the expected type of `s` in the notation is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't or there is no `s` in the notation, elaborate as a `Set`. There is currently a gotcha that elaboration to `Set` is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset).

mathlib-bors · 2024-08-16T01:47:26Z

Pull request successfully merged into master.

Build succeeded:

Define elaborators (but no delaborators) to elaborate the following notations to a `Finset`: In `Data.Finset.Basic`, * `{x ∈ s | p x}` In `Data.Fintype.Basic`, * `{x | p x}` * `{x : α | p x}` * `{x ∉ s | p x}` * `{x ≠ a | p x}` In `Order.Interval.Finset.Basic`, * `{x ≤ a | p x}` * `{x ≥ a | p x}` * `{x < a | p x}` * `{x > a | p x}` The general heuristic for deciding whether to elaborate a given notation as a `Set` or `Finset` is: * Check whether the expected type is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't, check whether the expected type of `s` in the notation is `Finset ?α`. * If it is, elaborate as a `Finset`. * If it isn't or there is no `s` in the notation, elaborate as a `Set`. There is currently a gotcha that elaboration to `Set` is highly preferred because we can't postpone metavariable and override the set elaborator without breaking many existing uses of set builder notation. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset).

YaelDillies added WIP Work in progress t-meta Tactics, attributes or user commands labels Mar 22, 2024

github-actions bot reviewed Mar 23, 2024

View reviewed changes

Mathlib/Data/List/Pairwise.lean Outdated Show resolved Hide resolved

YaelDillies force-pushed the finset_builder branch 2 times, most recently from 777235c to d9f35cb Compare March 25, 2024 06:34

YaelDillies added awaiting-review and removed WIP Work in progress labels Mar 25, 2024

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 7, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2024

YaelDillies force-pushed the finset_builder branch from c55d1dc to d5acd6e Compare May 27, 2024 10:59

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2024

YaelDillies changed the title ~~Feat: Finset builder notation~~ feat: Finset builder notation May 27, 2024

Vierkantor reviewed May 29, 2024

View reviewed changes

Mathlib/Data/Finset/Basic.lean Outdated Show resolved Hide resolved

Vierkantor reviewed May 29, 2024

View reviewed changes

Mathlib/Data/Fintype/Basic.lean Outdated Show resolved Hide resolved

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 29, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 30, 2024

YaelDillies force-pushed the finset_builder branch from f7d2f35 to cad709c Compare June 11, 2024 17:54

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 11, 2024

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Jun 11, 2024

joneugster reviewed Aug 13, 2024

View reviewed changes

Mathlib/Combinatorics/Enumerative/DoubleCounting.lean Show resolved Hide resolved

test/finset_builder.lean Show resolved Hide resolved

Mathlib/Data/Fintype/Basic.lean Show resolved Hide resolved

Mathlib/Data/Fintype/Basic.lean Outdated Show resolved Hide resolved

joneugster self-assigned this Aug 13, 2024

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 13, 2024

YaelDillies added 2 commits August 14, 2024 09:04

Merge branch 'master' into finset_builder

9189704

fix

ad25974

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 14, 2024

joneugster reviewed Aug 15, 2024

View reviewed changes

test/finset_builder.lean Outdated Show resolved Hide resolved

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 15, 2024

more exhaustive test suite

985d7de

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 15, 2024

github-actions bot added the maintainer-merge label Aug 15, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 15, 2024

kmill reviewed Aug 15, 2024

View reviewed changes

mathlib-bors bot changed the title ~~feat: Finset builder notation~~ [Merged by Bors] - feat: Finset builder notation Aug 16, 2024

mathlib-bors bot closed this Aug 16, 2024

mathlib-bors bot deleted the finset_builder branch August 16, 2024 01:47

YaelDillies mentioned this pull request Oct 6, 2024

[Merged by Bors] - feat(Algebra/MvPolynomial): Schwartz-Zippel lemma #5297

Closed

14 tasks

eric-wieser mentioned this pull request Oct 7, 2024

Update to Lean 4.11.0 trishullab/PutnamBench#222

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: Finset builder notation #11582

[Merged by Bors] - feat: Finset builder notation #11582

YaelDillies commented Mar 22, 2024 •

edited

Loading

YaelDillies commented May 29, 2024

github-actions bot commented Jun 11, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

YaelDillies commented Jun 11, 2024

joneugster left a comment

joneugster commented Aug 15, 2024

github-actions bot commented Aug 15, 2024

kmill commented Aug 15, 2024

kmill Aug 15, 2024

YaelDillies Aug 16, 2024

mathlib-bors bot commented Aug 15, 2024

mathlib-bors bot commented Aug 16, 2024

mathlib-bors bot commented Aug 16, 2024

[Merged by Bors] - feat: Finset builder notation #11582

[Merged by Bors] - feat: Finset builder notation #11582

Conversation

YaelDillies commented Mar 22, 2024 • edited Loading

YaelDillies commented May 29, 2024

github-actions bot commented Jun 11, 2024 • edited Loading

PR summary 985d7de269

Import changes for modified files

Declarations diff

YaelDillies commented Jun 11, 2024

joneugster left a comment

Choose a reason for hiding this comment

joneugster commented Aug 15, 2024

github-actions bot commented Aug 15, 2024

kmill commented Aug 15, 2024

kmill Aug 15, 2024

Choose a reason for hiding this comment

YaelDillies Aug 16, 2024

Choose a reason for hiding this comment

mathlib-bors bot commented Aug 15, 2024

mathlib-bors bot commented Aug 16, 2024

mathlib-bors bot commented Aug 16, 2024

YaelDillies commented Mar 22, 2024 •

edited

Loading

github-actions bot commented Jun 11, 2024 •

edited

Loading