[Merged by Bors] - feat: define Descriptive.Tree by sven-manthe · Pull Request #18763 · leanprover-community/mathlib4

sven-manthe · 2024-11-08T11:47:03Z

Define trees in the sense of descriptive set theory. Deduce SetLike from a more general instance about complete sublattices of power set lattices.
Taken from https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean

github-actions · 2024-11-08T11:47:51Z

messageFile.md

grunweg

Some stylistic comments. I don't know the mathematics behind this.

General questions/suggestions: can you link to some branch using this definition, to convince reviewers your design choices are workable? Is there some "easy" API you can include already? Definitions without API are always harder to review.

Mathlib/Order/CompleteLattice/SetLike.lean

grunweg · 2024-11-27T21:26:47Z

Mathlib/Order/CompleteLattice/SetLike.lean

+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sven Manthe
+-/
+import Mathlib.Order.CompleteSublattice


Is there a reason this is not in the CompleteSublattice file? Do you expect more material to join this file?

The main reason is that I expect that most users of CompleteSublattice don't need this file.

Hm. I see where you're coming from, but I'm not sure if this is common practice in mathlib... I'll wait for other reviewers to chime in.

Mathlib/Order/CompleteLattice/SetLike.lean

Mathlib/SetTheory/Descriptive/Tree.lean

Mathlib/Order/CompleteLattice/SetLike.lean

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

sven-manthe · 2024-11-29T16:52:12Z

I didn't provide more API yet to keep the PR short for review, but could change this of course. I don't want to create too many dependent branches (in theory, the code using this definition is public in the mentioned repository)

grunweg · 2024-11-29T17:02:17Z

I didn't provide more API yet to keep the PR short for review, but could change this of course. I don't want to create too many dependent branches (in theory, the code using this definition is public in the mentioned repository)

I see. At the moment, you have basically no API for the new definition. I think that probably errs on the side of "too little". Is there a modest amount of API you can sensibly add? If not, can you provide some pointers to where this is used? If I am to review this PR, looking through several thousand lines of code is not so nice.

sven-manthe · 2024-11-29T22:24:07Z

I'll try to add some API later. About pointers: The basic API is in the file https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean/blob/master/BorelDet/Tree/trees.lean

Mathlib/Order/CompleteLattice/SetLike.lean

Mathlib/SetTheory/Descriptive/Tree.lean

urkud · 2025-01-13T01:45:08Z

Is there a reason to use this design, as opposed to the usual carrier etc design of other SetLike structures? Also, should we have SetLike for any subtype of Set _?

sven-manthe · 2025-01-13T11:56:43Z

Is there a reason to use this design, as opposed to the usual carrier etc design of other SetLike structures?

Originally I worked with an inductive type, and provided manually SetLike and CompleteLattice instances and a complete lattice morphism. The current design is my attempt to prove the lemmas about the interaction between the SetLike and the lattice structure in the proper general context - there was no difference in using either design at least in my applications

sven-manthe · 2025-01-13T11:57:45Z

Also, should we have SetLike for any subtype of Set _?

I agree that there is nothing special about complete lattices here and in general, every weakening of complete Boolean algebras could be used

Mathlib/Order/CompleteLattice/SetLike.lean

eric-wieser · 2025-01-13T12:21:25Z

Also, should we have SetLike for any subtype of Set _?

My thinking would be "no", because this means we have a huge amount of API to duplicate between Subtype.val and SetLike.coe. So I'm also not sure we even want the single SetLike instance in this PR, and should instead just put up with having to write .val for now.

Mathlib/SetTheory/Descriptive/Tree.lean

sven-manthe · 2025-01-13T13:11:47Z

I agree with the comments here stating that the current design has problems (like duplication for subtypes of Set _), but don't know of a better design, so let me try to explain how I ended here: First, I definitely want the type of trees to be SetLike because this is used a lot later in my project. The complete sublattice structure is not as important, but worth recording. Thus, a design - that probably has none of the issues mentioned above - would be to make Tree A an inductive type and add SetLike and CompleteLattice for this type. The current approach achieves the same results for the type of trees (with almost identical code), but also adds some API for analogous types (admittedly, only for complete sublattices and not other subtypes of Set _). This additional API should not be a disadvantage in any situation - at least as long as no global instances are registered.

fpvandoorn · 2025-01-22T17:34:06Z

I've advised Sven on this project, but not on these particular definitions (I think, or very long ago).

Honestly I think the design here is fine:

The fact that it is a complete sublattice instead of a subtype/structure: this is also done in e.g. MeasureTheory.Lp
Normally, a SetLike instance is created just for the newly defined type. Here Sven does it for any sublattice of sets, which potentially could be reused elsewhere, so I don't think that is bad.
It is indeed a bit arbitrary to only do this for CompleteSublattices of Set X, but there is no technical way to do this for any subtype of Set X that is as easy to use, right?
The code Sven linked above shows that it is ok to work with this definition.

Are there any other objections raised here? If not, shall we just merge this?

Mathlib/Order/CompleteLattice/SetLike.lean

Mathlib/SetTheory/Descriptive/Tree.lean

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

github-actions · 2025-01-25T15:03:31Z

messageFile.md

(please merge master: see Zulip)

Mathlib/Order/CompleteLattice/SetLike.lean

…nto sven-trees-dst-1

github-actions · 2025-01-25T18:20:29Z

messageFile.md

github-actions · 2025-01-25T18:36:09Z

PR summary bb370cd79d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.CompleteLattice.SetLike` (new file)	517
`Mathlib.SetTheory.Descriptive.Tree` (new file)	518

Declarations diff

+ ext
+ ext_mem
+ instSubtype
+ instSubtypeSet
+ instance (A : Type*) : SetLike (tree A) (List A) := SetLike.instSubtypeSet
+ mem_iInf
+ mem_iSup
+ mem_inf
+ mem_mk
+ mem_of_append
+ mem_of_prefix
+ mem_sInf
+ mem_sSup
+ mem_sup
+ mem_top
+ not_mem_bot
+ setLike_mem_coe
+ setLike_mem_inf
+ setLike_mem_mk
+ setLike_mem_sup
+ tree
+ tree_eq_bot
++ mem_subtype

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Order/CompleteLattice/SetLike.lean

Mathlib/Data/SetLike/Basic.lean

Mathlib/Order/CompleteLattice/SetLike.lean

alreadydone · 2025-01-25T20:56:32Z

Mathlib/Order/CompleteLattice/SetLike.lean

-@[simp] theorem mem_iInf : x ∈ ⨅ i : I, f i ↔ ∀ i : I, x ∈ f i := by simp [← mem_subtype]
-@[simp] theorem mem_inf : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T := by simp [← mem_subtype]
-@[simp] theorem mem_top : x ∈ (⊤ : L) := by simp [← mem_subtype]
+@[simp] lemma setLike_mem_coe : x ∈ T.val ↔ x ∈ T := Iff.rfl


This can probably be removed since it's just SetLike.mem_coe.

But not up to reducible equality, I guess (at least the proof by simp only [SetLike.mem_coe] fails)

Interesting, I've always thought they are reducibly equal ... I think we should prefer (T : Set X) over T.val.

sven-manthe · 2025-01-26T11:28:56Z

To keep everyone up-to-date: I now generalized the SetLike instance as proposed (originally, I thought this wouldn't work because of a misunderstanding about the coercions from sublattices to types). This allowed to phrase the lemmas about non-complete sublattices in the appropriate generality (arguably, there should be even more, but currently mathlib is missing the definitions of e.g. subsemilattices). Unfortunately, the simp lemmas still need to be duplicated, because the binary inf/sup of a complete sublattice is only non-reducibly equal to the binary inf/sup of its underlying sublattice

alreadydone · 2025-01-26T19:18:15Z

LGTM
maintainer delegate

github-actions · 2025-01-26T19:18:35Z

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

jcommelin · 2025-01-27T13:32:30Z

bors r+

Define trees in the sense of descriptive set theory. Deduce SetLike from a more general instance about complete sublattices of power set lattices. Taken from https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com> Co-authored-by: sven-manthe <sven.manthe@uni-bonn.de>

mathlib-bors · 2025-01-27T14:51:04Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

define trees

f117e85

fix import all

64508e0

sven-manthe added the t-logic Logic (model theory, etc) label Nov 13, 2024

grunweg reviewed Nov 27, 2024

View reviewed changes

sven-manthe and others added 4 commits November 29, 2024 17:34

Update Mathlib/Order/CompleteLattice/SetLike.lean

a3d528a

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Update Mathlib/SetTheory/Descriptive/Tree.lean

2d43a0f

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Merge branch 'master' into sven-trees-dst-1

9535e19

minor style

eae3c5b

expand docstring

6f6ccb9

eric-wieser reviewed Jan 10, 2025

View reviewed changes

Mathlib/Order/CompleteLattice/SetLike.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 10, 2025

View reviewed changes

Mathlib/SetTheory/Descriptive/Tree.lean Outdated Show resolved Hide resolved

clarify docs

aeed48e

eric-wieser reviewed Jan 13, 2025

View reviewed changes

Mathlib/Order/CompleteLattice/SetLike.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 13, 2025

View reviewed changes

Mathlib/SetTheory/Descriptive/Tree.lean Outdated Show resolved Hide resolved

alreadydone reviewed Jan 25, 2025

View reviewed changes

Mathlib/Order/CompleteLattice/SetLike.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Descriptive/Tree.lean Outdated Show resolved Hide resolved

Mathlib/SetTheory/Descriptive/Tree.lean Outdated Show resolved Hide resolved

sven-manthe and others added 2 commits January 25, 2025 16:01

use calligraphic letter

9bd62fd

Update Mathlib/SetTheory/Descriptive/Tree.lean

75e319f

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone reviewed Jan 25, 2025

View reviewed changes

Mathlib/Order/CompleteLattice/SetLike.lean Outdated Show resolved Hide resolved

generalize setlike

4657e36

Merge remote-tracking branch 'refs/remotes/origin/sven-trees-dst-1' i…

96583a0

…nto sven-trees-dst-1

sven-manthe added 2 commits January 25, 2025 19:34

Merge branch 'master' into sven-trees-dst-1

237c278

minor

cfc06ee

sven-manthe added 2 commits January 25, 2025 19:39

fix

be7adab

minor

2e84fc4

sven-manthe added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 25, 2025

alreadydone reviewed Jan 25, 2025

View reviewed changes

rework

2fccba9

sven-manthe removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 26, 2025

fix missing simp

f47e709

sven-manthe added 2 commits January 26, 2025 18:22

add lemma to use import

b53b6ca

style

bb370cd

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 26, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 27, 2025

mathlib-bors bot changed the title ~~feat: define Descriptive.Tree~~ [Merged by Bors] - feat: define Descriptive.Tree Jan 27, 2025

mathlib-bors bot closed this Jan 27, 2025

mathlib-bors bot deleted the sven-trees-dst-1 branch January 27, 2025 14:51

Conversation

sven-manthe commented Nov 8, 2024

Uh oh!

github-actions bot commented Nov 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg Nov 27, 2024

Choose a reason for hiding this comment

Uh oh!

sven-manthe Nov 29, 2024

Choose a reason for hiding this comment

Uh oh!

grunweg Nov 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sven-manthe commented Nov 29, 2024

Uh oh!

grunweg commented Nov 29, 2024

Uh oh!

sven-manthe commented Nov 29, 2024

Uh oh!

Uh oh!

Uh oh!

urkud commented Jan 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sven-manthe commented Jan 13, 2025

Uh oh!

sven-manthe commented Jan 13, 2025

Uh oh!

Uh oh!

eric-wieser commented Jan 13, 2025

Uh oh!

Uh oh!

sven-manthe commented Jan 13, 2025

Uh oh!

fpvandoorn commented Jan 22, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 25, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 25, 2025

Uh oh!

github-actions bot commented Jan 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary bb370cd79d

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

alreadydone Jan 25, 2025

Choose a reason for hiding this comment

Uh oh!

sven-manthe Jan 26, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jan 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sven-manthe commented Jan 26, 2025

github-actions bot commented Nov 8, 2024 •

edited

Loading

grunweg Nov 29, 2024 •

edited

Loading

urkud commented Jan 13, 2025 •

edited

Loading

github-actions bot commented Jan 25, 2025 •

edited by alreadydone

Loading

github-actions bot commented Jan 25, 2025 •

edited

Loading

alreadydone Jan 26, 2025 •

edited

Loading