Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(SetTheory): Upper bound for games #10566

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(SetTheory): Upper bound for games #10566

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6dd5c1c
feat(SetTheory/Game): define `PGame.upperBound`
YaelDillies Feb 14, 2024
99d4af5
inline
YaelDillies Feb 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
39 changes: 38 additions & 1 deletion Mathlib/SetTheory/Game/PGame.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@
import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Basic
import Mathlib.Logic.Relation
import Mathlib.Logic.Small.Defs
import Mathlib.Order.GameAdd

#align_import set_theory.game.pgame from "leanprover-community/mathlib"@"dc9e5ba64653e017743ba5d2c28e42f9f486bf99"
#align_import set_theory.game.pgame from "leanprover-community/mathlib"@"8900d545017cd21961daa2a1734bb658ef52c618"

Check notice on line 12 in Mathlib/SetTheory/Game/PGame.lean

View workflow job for this annotation

GitHub Actions / Add annotations

Synchronization 

See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/set_theory/game/pgame?range=dc9e5ba64653e017743ba5d2c28e42f9f486bf99..8900d545017cd21961daa2a1734bb658ef52c618

/-!
# Combinatorial (pre-)games.
Expand Down Expand Up @@ -731,6 +732,42 @@
Classical.choose_spec <| (zero_le.1 h) j
#align pgame.left_response_spec SetTheory.PGame.leftResponse_spec

#noalign pgame.upper_bound
#noalign pgame.upper_bound_right_moves_empty
#noalign pgame.le_upper_bound
#noalign pgame.upper_bound_mem_upper_bounds

/-- A small family of pre-games is bounded above. -/
lemma bddAbove_range_of_small [Small.{u} ι] (f : ι → PGame.{u}) : BddAbove (Set.range f) := by
let x : PGame.{u} := ⟨Σ i, (f $ (equivShrink.{u} ι).symm i).LeftMoves, PEmpty,
fun x ↦ moveLeft _ x.2, PEmpty.elim⟩
refine ⟨x, Set.forall_range_iff.2 fun i ↦ ?_⟩
rw [← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]
simpa using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩
Comment on lines +740 to +746
Copy link
Collaborator

Choose a reason for hiding this comment

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

This is a specialization of bddAbove_of_small to small_range. (Although the small_range instance is not currently in scope because we only import Logic.Small.Defs.) Is it really worth exposing as a separate lemma? I suppose the benefit of having it as a seperate lemma is that it makes the proof of bddAbove_of_small more modular. This seems like a tradeoff between API clutter and proof modularity. What is the usual stance on this tradeoff in mathlib? Maybe we can get the best of both worlds by marking this as a private lemma?

Copy link
Collaborator

Choose a reason for hiding this comment

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

On the other hand, maybe this lemma is good for searchability? A user might be expecting to prove BddAbove via a family and not know what Small means so fail to identify that bddAbove_of_small is applicable?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Most predicates in mathlib come in two kinds: A set version and an indexed version. You can define IsFooSet s as IsFooFamily (Subtype.val : s → α) and you can define IsFooFamily f as IsFooSet (Set.range f) (assuming duplicates in your family don't matter). However, it is usually impractical to use one predicate in place of the other:

  • When using IsFooFamily (Subtype.val : s → α), elements of s are now images of the coercion Subtype.val : s → α
  • When using IsFooSet (Set.range f), you need to replace y ∈ Set.range f by f x, x and vice-versa.

It is therefore preferrable to have both predicates (see eg IsDirected). This is currently not the case for BddAbove, where we only have the set version. Hence I am acting as if BddAbove (Set.range _) was a predicate, because many lemmas expect it in that form and because it might become one in the future. The fact that bddAbove_range_of_small can be syntactically derived from bddAbove_of_small is somehow an accident of us not having the family predicate, and I would rather not muddle the waters by only having the set version of the lemma.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Interesting! Thanks for the explanation


/-- A small set of pre-games is bounded above. -/
lemma bddAbove_of_small (s : Set PGame.{u}) [Small.{u} s] : BddAbove s := by
simpa using bddAbove_range_of_small (Subtype.val : s → PGame.{u})
#align pgame.bdd_above_of_small SetTheory.PGame.bddAbove_of_small

#noalign pgame.lower_bound
#noalign pgame.lower_bound_left_moves_empty
#noalign pgame.lower_bound_le
#noalign pgame.lower_bound_mem_lower_bounds

/-- A small family of pre-games is bounded below. -/
lemma bddBelow_range_of_small [Small.{u} ι] (f : ι → PGame.{u}) : BddBelow (Set.range f) := by
YaelDillies marked this conversation as resolved.
Show resolved Hide resolved
let x : PGame.{u} := ⟨PEmpty, Σ i, (f $ (equivShrink.{u} ι).symm i).RightMoves, PEmpty.elim,
fun x ↦ moveRight _ x.2⟩
refine ⟨x, Set.forall_range_iff.2 fun i ↦ ?_⟩
rw [← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]
simpa using fun j ↦ @lf_moveRight x ⟨equivShrink ι i, j⟩

/-- A small set of pre-games is bounded below. -/
lemma bddBelow_of_small (s : Set PGame.{u}) [Small.{u} s] : BddBelow s := by
simpa using bddBelow_range_of_small (Subtype.val : s → PGame.{u})
#align pgame.bdd_below_of_small SetTheory.PGame.bddBelow_of_small

/-- The equivalence relation on pre-games. Two pre-games `x`, `y` are equivalent if `x ≤ y` and
`y ≤ x`.

Expand Down