[Merged by Bors] - feat(Order/Comparable): comparability/incomparability relations by vihdzp · Pull Request #19580 · leanprover-community/mathlib4

vihdzp · 2024-11-28T20:51:25Z

We define two new relations for comparability and incomparability in a preorder, and introduce basic API for them. See this comment for an explanation of why we want both.

This will be used in the new CGT repo to define the fuzzy relation x ‖ y = IncompRel (· ≤ ·) x y.

depends on: [Merged by Bors] - feat(Order/Antisymmetrization): AntisymmRel lemmas #19571
depends on: [Merged by Bors] - chore: antisymm_refl → Antisymm.refl #21202

github-actions · 2024-11-28T20:52:20Z

PR summary 8de3a2ba06

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Comparable` (new file)	211

Declarations diff

+ AntisymmRel.compRel
+ AntisymmRel.compRel_congr
+ AntisymmRel.compRel_congr_left
+ AntisymmRel.compRel_congr_right
+ AntisymmRel.incompRel_congr
+ AntisymmRel.incompRel_congr_left
+ AntisymmRel.incompRel_congr_right
+ AntisymmRel.not_incompRel
+ AntisymmRel.trans_compRel
+ AntisymmRel.trans_incompRel
+ CompRel
+ CompRel.decidableRel
+ CompRel.of_antisymmRel_of_compRel
+ CompRel.of_compRel_of_antisymmRel
+ CompRel.of_ge
+ CompRel.of_gt
+ CompRel.of_le
+ CompRel.of_lt
+ CompRel.of_rel
+ CompRel.of_rel_symm
+ CompRel.refl
+ CompRel.rfl
+ CompRel.symm
+ CompRel.trans_antisymmRel
+ IncompRel
+ IncompRel.decidableRel
+ IncompRel.not_antisymmRel
+ IncompRel.not_ge
+ IncompRel.not_gt
+ IncompRel.not_le
+ IncompRel.not_lt
+ IncompRel.refl
+ IncompRel.rfl
+ IncompRel.symm
+ IncompRel.trans_antisymmRel
+ IsTotal.compRel
+ IsTotal.not_incompRel
+ LE.le.compRel
+ LE.le.compRel_symm
+ LE.le.not_incompRel
+ LT.lt.compRel
+ LT.lt.compRel_symm
+ LT.lt.not_incompRel
+ antisymmRel_compl
+ antisymmRel_compl_apply
+ antisymmRel_swap_apply
+ compRel_comm
+ compRel_swap
+ compRel_swap_apply
+ incompRel_comm
+ incompRel_compl
+ incompRel_compl_apply
+ incompRel_of_antisymmRel_of_incompRel
+ incompRel_of_incompRel_of_antisymmRel
+ incompRel_swap
+ incompRel_swap_apply
+ instance : @Trans α α α (AntisymmRel (· ≤ ·)) (CompRel (· ≤ ·)) (CompRel (· ≤ ·))
+ instance : @Trans α α α (AntisymmRel (· ≤ ·)) (IncompRel (· ≤ ·)) (IncompRel (· ≤ ·))
+ instance : @Trans α α α (CompRel (· ≤ ·)) (AntisymmRel (· ≤ ·)) (CompRel (· ≤ ·))
+ instance : @Trans α α α (IncompRel (· ≤ ·)) (AntisymmRel (· ≤ ·)) (IncompRel (· ≤ ·))
+ instance : IsSymm α (CompRel r)
+ instance : IsSymm α (IncompRel r)
+ instance [IsIrrefl α r] : IsRefl α (IncompRel r)
+ instance [IsRefl α r] : IsRefl α (CompRel r)
+ linearOrderOfComprel
+ lt_or_antisymmRel_or_gt_or_incompRel
+ lt_or_eq_or_gt_or_incompRel
+ not_compRel_iff
+ not_incompRel_iff
+ not_le_iff_lt_or_incompRel

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

jsm28 · 2024-11-29T00:51:15Z

If you do want to use a different symbol, U+01C1 LATIN LETTER LATERAL CLICK ǁ and U+23F8 DOUBLE VERTICAL BAR ⏸ are also options to consider.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

vihdzp · 2025-03-02T03:14:15Z

Perhaps we can reconsider having both CompRel and IncompRel? It might be obvious to us as mathematicians that ¬ (r x y ∨ r y x) ↔ ¬ r x y ∧ ¬ r y x, but this extra layer of indirection ends up making ¬ CompRel more inconvenient than IncompRel was. For instance, while we can use constructor notation ⟨h₁, h₂⟩ to build IncompRel, we can't do the same for ¬ CompRel - we'd have to declare a theorem like not_compRel_of_not_rel to get the same thing done.

Also, I want to use this relation within game theory, and in that context, incomparability is by far the more natural notion. IncompRel (· ≤ ·) G 0 represents a concrete outcome for the game G: it is won by the first player. On the other hand, CompRel (· ≤ ·) G 0 represents one of three other outcomes: the game is won by the second player, or by Left, or by Right.

This duplication wouldn't be something without precedent. After all, we have both Finite and Infinite in Mathlib and no one has complained yet.

b-mehta · 2025-03-03T18:54:13Z

Thinking about this more, I agree with you. Another nice example is Subsingleton and Nontrivial, where we have both, and they're expressed in a more interesting way than as the negation of the other. Let's go with both here too!

vihdzp · 2025-03-05T06:09:01Z

I've updated the PR yet again, to include both the comparability and incomparability relations.

YaelDillies

Thanks!

maintainer delegate

Mathlib/Order/Comparable.lean

github-actions · 2025-03-05T12:31:43Z

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

Mathlib/Order/Comparable.lean

b-mehta

bors d+

Thanks!

mathlib-bors · 2025-03-05T12:39:22Z

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

ghost · 2025-03-06T02:44:54Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

We define two new relations for comparability and incomparability in a preorder, and introduce basic API for them. See [this comment](#19580 (comment)) for an explanation of why we want both. This will be used in the new [CGT repo](https://github.com/vihdzp/combinatorial-games) to define the fuzzy relation `x ‖ y = IncompRel (· ≤ ·) x y`.

mathlib-bors · 2025-03-06T03:23:43Z

Pull request successfully merged into master.

Build succeeded:

We define two new relations for comparability and incomparability in a preorder, and introduce basic API for them. See [this comment](#19580 (comment)) for an explanation of why we want both. This will be used in the new [CGT repo](https://github.com/vihdzp/combinatorial-games) to define the fuzzy relation `x ‖ y = IncompRel (· ≤ ·) x y`.

vihdzp added 13 commits November 28, 2024 00:48

notation

0b58e49

Update Antisymmetrization.lean

fcc71a1

Update Antisymmetrization.lean

97d7c96

Update Antisymmetrization.lean

94479b4

start

dce79df

Update Antisymmetrization.lean

68b976e

Update Antisymmetrization.lean

050965a

Merge branch 'vi.antisymm' into vi.incomp

c1dfa0f

progress

35d27ba

instances

6011740

Merge branch 'vi.antisymm' into vi.incomp

c57d390

finish

f2d6e73

more

7a403d9

vihdzp added the t-order Order theory label Nov 28, 2024

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 28, 2024

vihdzp added 4 commits November 28, 2024 15:43

Merge branch 'vi.antisymm' into vi.incomp

eaba256

progress

20518ce

mk-all

b077e26

Update Antisymmetrization.lean

2ce6251

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

Update Antisymmetrization.lean

0d5c665

vihdzp mentioned this pull request Nov 28, 2024

Tracking issue: game order relations cleanup #19588

Closed

5 tasks

vihdzp and others added 6 commits December 11, 2024 04:46

undo notation :(

04626e8

undo notation again :'(

1219ba0

Merge branch 'vi.antisymm' into vi.incomp

37b370c

delete notation 😢

632eded

Update Mathlib/Order/Antisymmetrization.lean

964bff9

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge branch 'master' into vi.antisymm

baf6fd9

Update Mathlib/Order/Comparable.lean

ae1acd3

vihdzp added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 4, 2025

vihdzp added 2 commits March 4, 2025 23:02

Merge branch 'master' into vi.incomp

088da9d

Update Comparable.lean

256daac

vihdzp changed the title ~~feat(Order/Comparable): comparability relation~~ feat(Order/Comparable): comparability/incomparability relations Mar 5, 2025

vihdzp removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 5, 2025

vihdzp requested a review from b-mehta March 5, 2025 06:09

comm lemmas

a34adef

vihdzp mentioned this pull request Mar 5, 2025

feat: redefine x ‖ y as IncompRel x y vihdzp/combinatorial-games#53

Merged

YaelDillies approved these changes Mar 5, 2025

View reviewed changes

Mathlib/Order/Comparable.lean Outdated Show resolved Hide resolved

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

b-mehta reviewed Mar 5, 2025

View reviewed changes

Mathlib/Order/Comparable.lean Show resolved Hide resolved

b-mehta reviewed Mar 5, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 5, 2025

apply suggestins

8de3a2b

vihdzp added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 6, 2025

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

mathlib-bors bot changed the title ~~feat(Order/Comparable): comparability/incomparability relations~~ [Merged by Bors] - feat(Order/Comparable): comparability/incomparability relations Mar 6, 2025

mathlib-bors bot closed this Mar 6, 2025

mathlib-bors bot deleted the vi.incomp branch March 6, 2025 03:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Order/Comparable): comparability/incomparability relations#19580

[Merged by Bors] - feat(Order/Comparable): comparability/incomparability relations#19580
vihdzp wants to merge 71 commits intomasterfrom
vi.incomp

vihdzp commented Nov 28, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 28, 2024 •

edited

Loading

Declarations diff

Uh oh!

jsm28 commented Nov 29, 2024

Uh oh!

vihdzp commented Mar 2, 2025 •

edited

Loading

Uh oh!

b-mehta commented Mar 3, 2025

Uh oh!

vihdzp commented Mar 5, 2025

Uh oh!

YaelDillies left a comment

Uh oh!

Uh oh!

github-actions bot commented Mar 5, 2025

Uh oh!

Uh oh!

b-mehta left a comment

Uh oh!

mathlib-bors bot commented Mar 5, 2025

Uh oh!

ghost commented Mar 6, 2025

Uh oh!

mathlib-bors bot commented Mar 6, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 8de3a2ba06

Import changes for modified files

Declarations diff

Uh oh!

jsm28 commented Nov 29, 2024

Uh oh!

vihdzp commented Mar 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

b-mehta commented Mar 3, 2025

Uh oh!

vihdzp commented Mar 5, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Mar 5, 2025

Uh oh!

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 5, 2025

Uh oh!

ghost commented Mar 6, 2025

Uh oh!

mathlib-bors bot commented Mar 6, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

vihdzp commented Nov 28, 2024 •

edited

Loading

github-actions bot commented Nov 28, 2024 •

edited

Loading

vihdzp commented Mar 2, 2025 •

edited

Loading