[Merged by Bors] - feat(Data/List/ReduceOption): add replicate theorems by anthonyde · Pull Request #20644 · leanprover-community/mathlib4

anthonyde · 2025-01-10T21:11:40Z

These theorems make it easier to prove statements about List.reduceOption, building up to a more general theorem, reduceOption_eq_concat_iff, which is useful for inductive proofs.

These theorems make it easier to prove statements about `List.reduceOption`, building up to a more general theorem, `reduceOption_eq_concat_iff`, which is useful for inductive proofs.

github-actions · 2025-01-10T21:12:31Z

PR summary 2c5572490e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ reduceOption_eq_append_iff
+ reduceOption_eq_concat_iff
+ reduceOption_eq_nil_iff
+ reduceOption_eq_singleton_iff
+ reduceOption_replicate_none

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/Data/List/ReduceOption.lean

kim-em · 2025-01-11T04:09:06Z

Besides naming issues, looks good to me, thank you!

bors d+

mathlib-bors · 2025-01-11T04:09:08Z

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

`reduceOption_replicate_of_none` -> `reduceOption_replicate_none` `reduceOption_eq_nil_replicate_iff` -> `reduceOption_eq_nil_iff` `reduceOption_eq_singleton_replicate_iff` -> `reduceOption_eq_singleton_iff`

Theorems were renamed.

anthonyde · 2025-01-11T13:16:20Z

Thanks for the review!

bors merge

These theorems make it easier to prove statements about `List.reduceOption`, building up to a more general theorem, `reduceOption_eq_concat_iff`, which is useful for inductive proofs.

mathlib-bors · 2025-01-11T13:24:44Z

Pull request successfully merged into master.

Build succeeded:

Theorems were renamed.

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

Theorems were renamed.

feat(Data/List/ReduceOption): add replicate theorems

c159aff

These theorems make it easier to prove statements about `List.reduceOption`, building up to a more general theorem, `reduceOption_eq_concat_iff`, which is useful for inductive proofs.

anthonyde added the t-data Data (lists, quotients, numbers, etc) label Jan 10, 2025

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jan 10, 2025

This was referenced Jan 10, 2025

[Merged by Bors] - feat(Computability/EpsilonNFA): define path relation #20645

Closed

feat: formalize regular expression -> εNFA #20648

Open

kim-em reviewed Jan 11, 2025

View reviewed changes

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

kim-em reviewed Jan 11, 2025

View reviewed changes

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

kim-em reviewed Jan 11, 2025

View reviewed changes

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

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 11, 2025

Use suggested theorem names

2c55724

`reduceOption_replicate_of_none` -> `reduceOption_replicate_none` `reduceOption_eq_nil_replicate_iff` -> `reduceOption_eq_nil_iff` `reduceOption_eq_singleton_replicate_iff` -> `reduceOption_eq_singleton_iff`

anthonyde added a commit to anthonyde/mathlib4 that referenced this pull request Jan 11, 2025

Fix for changes in leanprover-community#20644

0b03c95

Theorems were renamed.

anthonyde added a commit to anthonyde/mathlib4 that referenced this pull request Jan 11, 2025

Fix for changes in leanprover-community#20644

138c815

Theorems were renamed.

mathlib-bors bot changed the title ~~feat(Data/List/ReduceOption): add replicate theorems~~ [Merged by Bors] - feat(Data/List/ReduceOption): add replicate theorems Jan 11, 2025

mathlib-bors bot closed this Jan 11, 2025

mathlib-bors bot deleted the anthonyde/list-replicate branch January 11, 2025 13:24

anthonyde added a commit that referenced this pull request Jan 11, 2025

Fix for changes in #20644

e73681c

Theorems were renamed.

anthonyde added a commit that referenced this pull request Jan 11, 2025

Fix for changes in #20644

dbc35ee

Theorems were renamed.

anthonyde added a commit that referenced this pull request Jan 20, 2025

Fix for changes in #20644

4aade4c

Theorems were renamed.

anthonyde added a commit to anthonyde/mathlib4 that referenced this pull request Feb 6, 2025

Fix for changes in leanprover-community#20644

9169457

Theorems were renamed.

anthonyde added a commit that referenced this pull request Feb 19, 2025

Fix for changes in #20644

d5c2955

Theorems were renamed.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Data/List/ReduceOption): add replicate theorems#20644

[Merged by Bors] - feat(Data/List/ReduceOption): add replicate theorems#20644
anthonyde wants to merge 2 commits intomasterfrom
anthonyde/list-replicate

anthonyde commented Jan 10, 2025

Uh oh!

github-actions bot commented Jan 10, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

anthonyde commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

anthonyde commented Jan 10, 2025

Uh oh!

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

Uh oh!

PR summary 2c5572490e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

anthonyde commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Jan 10, 2025 •

edited

Loading