[Merged by Bors] - feat(SetTheory): Upper bound for games #10566
Conversation
YaelDillies
added
awaiting-review
YaelDillies
changed the title
PGame.upperBound
There was a problem hiding this comment.
Thanks for the forward port! I'm trying to pitch in with a review as someone with an interest in CGT. This is indeed a faithful forward port of the pgame.lean changes in leanprover-community/mathlib#15260, so while I do have some requested changes, I don't mind if we merge this and save my feedback for a future PR.
| /-- 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⟩ |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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 ofsare now images of the coercionSubtype.val : s → α - When using
IsFooSet (Set.range f), you need to replacey ∈ Set.range fbyf x,xand 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.
There was a problem hiding this comment.
Interesting! Thanks for the explanation
leanprover-community-mathlib4-bot
added
ready-to-merge
Partially forward-port leanprover-community/mathlib#15260
|
Build failed (retrying...):
|
Partially forward-port leanprover-community/mathlib#15260
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Partially forward-port leanprover-community/mathlib#15260
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Partially forward-port leanprover-community/mathlib#15260
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Partially forward-port leanprover-community/mathlib#15260
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Partially forward-port leanprover-community/mathlib#15260
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>
Partially forward-port leanprover-community/mathlib#15260