Skip to content

[Merged by Bors] - feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness#19555

Closed
tristan-f-r wants to merge 5 commits intomasterfrom
tristanfr.relatorlem
Closed

[Merged by Bors] - feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness#19555
tristan-f-r wants to merge 5 commits intomasterfrom
tristanfr.relatorlem

Conversation

@tristan-f-r
Copy link
Copy Markdown
Collaborator

@tristan-f-r tristan-f-r commented Nov 28, 2024

Adds left, right, and bi_total_empty, and golfs identical_of_isEmpty in PGame as a result.

Open in Gitpod

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 28, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 28, 2024 •
edited
Loading

PR summary 6d5870b1c6

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Logic.IsEmpty 91 92 +1 (+1.10%)
Import changes for all files
Files Import difference
87 files Mathlib.Algebra.Group.WithOne.Defs Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.Group.Commute.Hom Mathlib.Tactic.FunProp Mathlib.Algebra.Group.Hom.Basic Mathlib.Data.Nat.Bits Mathlib.Tactic.Widget.CongrM Mathlib.Algebra.Divisibility.Units Mathlib.Data.Rat.Defs Mathlib.Data.Nat.Factorial.Basic Mathlib.Data.Int.Defs Mathlib.Tactic.FunProp.RefinedDiscrTree Mathlib.Logic.Equiv.Pairwise Mathlib.Tactic.FunProp.Elab Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Data.PNat.Defs Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.InjSurj Mathlib.Tactic.FunProp.Theorems Mathlib.Order.ULift Mathlib.Logic.Unique Mathlib.Data.Nat.Prime.Factorial Mathlib.Data.List.Count Mathlib.Data.Matrix.DMatrix Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Logic.Pairwise Mathlib.Tactic.Common Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Basic Mathlib.Tactic.MoveAdd Mathlib.Data.Int.Cast.Basic Mathlib.Algebra.GroupWithZero.Divisibility Mathlib.Algebra.GroupWithZero.Commute Mathlib.Logic.IsEmpty Mathlib.Algebra.Group.Hom.Instances Mathlib.Control.Bifunctor Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Tactic.CongrExclamation Mathlib.Algebra.Ring.Idempotents Mathlib.Tactic.Convert Mathlib.Tactic.FunProp.Attr Mathlib.Logic.Lemmas Mathlib.Algebra.GroupWithZero.Pi Mathlib.Control.Bitraversable.Lemmas Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Order.RelClasses Mathlib.Algebra.Ring.Ext Mathlib.Control.Bitraversable.Basic Mathlib.Algebra.Prime.Defs Mathlib.Order.Basic Mathlib.Tactic.ContinuousFunctionalCalculus Mathlib.Topology.ContinuousMap.Defs Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Lean.Meta.CongrTheorems Mathlib.Algebra.Quotient Mathlib.Tactic.Nontriviality.Core Mathlib.Algebra.Order.Sum Mathlib.Data.Nat.Size Mathlib.Algebra.Group.Commute.Basic Mathlib.Data.Sigma.Lex Mathlib.Data.Nat.Prime.Defs Mathlib.Algebra.Group.Commute.Units Mathlib.Deprecated.RelClasses Mathlib.Tactic.FunProp.Core Mathlib.Data.Int.Sqrt Mathlib.Data.Nat.PSub Mathlib.Algebra.Group.Nat.Units Mathlib.Control.Bitraversable.Instances Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Pi.Basic Mathlib.Data.Vector.Defs Mathlib.Data.Nat.GCD.Basic Mathlib.Tactic.TermCongr Mathlib.Algebra.Group.Hom.Defs Mathlib.Tactic.Zify Mathlib.Algebra.Field.IsField Mathlib.Algebra.Divisibility.Basic Mathlib.Logic.Nontrivial.Basic Mathlib.Tactic.CongrM Mathlib.Topology.Defs.Basic Mathlib.Tactic.Nontriviality
 1

Declarations diff

+ biTotal_empty
+ leftTotal_empty
+ rightTotal_empty

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).

vihdzp
vihdzp reviewed Nov 28, 2024
View reviewed changes
@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Nov 28, 2024

Can you add these lemmas in another file? Logic.Relator is a very basic file and you're nearly tripling its import amount. Perhaps Logic.IsEmpty works?

@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 28, 2024
@tristan-f-r @vihdzp
fix(Logic): move Relator -> IsEmpty, clean up proofs
ddea69b 
Co-Authored-By: Violeta Hernández <vi.hdz.p@gmail.com>
@tristan-f-r
Copy link
Copy Markdown
Collaborator Author

tristan-f-r commented Nov 28, 2024

Unsure if there are good ways to reduce the simp to apply, but I couldn't successfully reduce the proofs with your suggestion or similar modifications of it.

@tristan-f-r tristan-f-r changed the title feat(Logic/Relator): Left/Right/BiTotal truthiness on emptiness feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness Nov 28, 2024
vihdzp
vihdzp approved these changes Nov 28, 2024
View reviewed changes
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise, this all LGTM.

tristan-f-r and others added 2 commits November 28, 2024 16:31
@tristan-f-r @vihdzp
chore(Mathlib/Logic/IsEmpty): shorter variable declaration
ac68362 
Uses Type* to implicitly create universe variables

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
@tristan-f-r @vihdzp
chore(SetTheory/Game/PGame): remove unnecessary IsEmpty import
6d5870b 
Co-Authored-By: Violeta Hernández <vi.hdz.p@gmail.com>
@tristan-f-r tristan-f-r added the t-set-theory Set theory label Nov 29, 2024
@tristan-f-r tristan-f-r requested a review from b-mehta November 30, 2024 23:18
@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Nov 30, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 1, 2024

Here are the benchmark results for commit 6d5870b.
There were no significant changes against commit 73295cb.

@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented Dec 2, 2024

Hmm, I'm slightly worried about simp ending up spending ages trying to prove IsEmpty when it gets called on something involving Left/Right/Bi Total things, but the benchmark doesn't seem to back this up. So let's go with it for now.

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 2, 2024
@tristan-f-r
feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness (#19555)
09ceeef 
Adds left, right, and bi_total_empty, and golfs `identical_of_isEmpty` in `PGame` as a result.



Co-authored-by: Tristan F. <LeoDog896@hotmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness [Merged by Bors] - feat(Logic/IsEmpty): Left/Right/BiTotal truthiness on emptiness Dec 2, 2024
@mathlib-bors mathlib-bors bot closed this Dec 2, 2024
@mathlib-bors mathlib-bors bot deleted the tristanfr.relatorlem branch December 2, 2024 16:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta Awaiting requested review from b-mehta

1 more reviewer

@vihdzp vihdzp vihdzp approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@tristan-f-r @vihdzp @b-mehta @leanprover-bot