feat: dominated moves, reversible moves, and gift horses#124
Open
plp127 wants to merge 27 commits intovihdzp:masterfrom
Open
feat: dominated moves, reversible moves, and gift horses#124plp127 wants to merge 27 commits intovihdzp:masterfrom
plp127 wants to merge 27 commits intovihdzp:masterfrom
Conversation
tristan-f-r
reviewed
Jul 13, 2025
Comment on lines
26
to
110
| theorem equiv_of_bypass_left {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | ||
| {c cr : ι → IGame.{u}} (hbb : ∀ i, cr i ≤ {Set.range c ∪ l | r}ᴵ) | ||
| (hcr : ∀ i, cr i ∈ (c i).rightMoves) : | ||
| {Set.range c ∪ l | r}ᴵ ≈ {(⋃ i, (cr i).leftMoves) ∪ l | r}ᴵ := by | ||
| constructor | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| rw [leftMoves_ofSets] at hz | ||
| obtain ⟨i, rfl⟩ | hz := hz | ||
| · refine lf_of_rightMove_le ?_ (hcr i) | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rw [leftMoves_ofSets] | ||
| exact .inl (Set.mem_iUnion_of_mem i hz) | ||
| · intro z hz | ||
| apply not_le_of_le_of_not_le (hbb i) | ||
| apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] at hz ⊢ | ||
| · apply lf_of_le_leftMove le_rfl | ||
| rw [leftMoves_ofSets] | ||
| exact .inr hz | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] at hz ⊢ | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| rw [leftMoves_ofSets] at hz | ||
| obtain ⟨_, ⟨i, rfl⟩, hz⟩ | hz := hz | ||
| · refine not_le_of_not_le_of_le ?_ (hbb i) | ||
| exact lf_of_le_leftMove le_rfl hz | ||
| · apply lf_of_le_leftMove le_rfl | ||
| rw [leftMoves_ofSets] | ||
| exact .inr hz | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] at hz ⊢ | ||
|
|
||
| theorem equiv_of_bypass_right {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | ||
| {d dl : ι → IGame.{u}} (hbb : ∀ i, {l | Set.range d ∪ r}ᴵ ≤ dl i) | ||
| (hdl : ∀ i, dl i ∈ (d i).leftMoves) : | ||
| {l | Set.range d ∪ r}ᴵ ≈ {l | (⋃ i, (dl i).rightMoves) ∪ r}ᴵ := by | ||
| constructor | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] at hz ⊢ | ||
| · intro z hz | ||
| rw [rightMoves_ofSets] at hz | ||
| obtain ⟨_, ⟨i, rfl⟩, hz⟩ | hz := hz | ||
| · apply not_le_of_le_of_not_le (hbb i) | ||
| exact lf_of_rightMove_le le_rfl hz | ||
| · apply lf_of_rightMove_le le_rfl | ||
| rw [rightMoves_ofSets] | ||
| exact .inr hz | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] at hz ⊢ | ||
| · intro z hz | ||
| rw [rightMoves_ofSets] at hz | ||
| obtain ⟨i, rfl⟩ | hz := hz | ||
| · refine lf_of_le_leftMove ?_ (hdl i) | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| refine not_le_of_not_le_of_le ?_ (hbb i) | ||
| apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] at hz ⊢ | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rw [rightMoves_ofSets] | ||
| exact .inl (Set.mem_iUnion_of_mem i hz) | ||
| · apply lf_of_rightMove_le le_rfl | ||
| rw [rightMoves_ofSets] | ||
| exact .inr hz |
Collaborator
There was a problem hiding this comment.
My initial golf of equiv_of_bypass which requires Mathlib.Algebra.Group.Pointwise.Set.Lattice. I can't find the essence of equiv_of_bypass_left in this proof, but some extension of the lemma leftMove_lf for ofSets should golf this down considerably more. Though, that's more of a question of if we want ofSets variants for any lemmas that use left/right sets membership.
Suggested change
| theorem equiv_of_bypass_left {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | |
| {c cr : ι → IGame.{u}} (hbb : ∀ i, cr i ≤ {Set.range c ∪ l | r}ᴵ) | |
| (hcr : ∀ i, cr i ∈ (c i).rightMoves) : | |
| {Set.range c ∪ l | r}ᴵ ≈ {(⋃ i, (cr i).leftMoves) ∪ l | r}ᴵ := by | |
| constructor | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| rw [leftMoves_ofSets] at hz | |
| obtain ⟨i, rfl⟩ | hz := hz | |
| · refine lf_of_rightMove_le ?_ (hcr i) | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rw [leftMoves_ofSets] | |
| exact .inl (Set.mem_iUnion_of_mem i hz) | |
| · intro z hz | |
| apply not_le_of_le_of_not_le (hbb i) | |
| apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] at hz ⊢ | |
| · apply lf_of_le_leftMove le_rfl | |
| rw [leftMoves_ofSets] | |
| exact .inr hz | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] at hz ⊢ | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| rw [leftMoves_ofSets] at hz | |
| obtain ⟨_, ⟨i, rfl⟩, hz⟩ | hz := hz | |
| · refine not_le_of_not_le_of_le ?_ (hbb i) | |
| exact lf_of_le_leftMove le_rfl hz | |
| · apply lf_of_le_leftMove le_rfl | |
| rw [leftMoves_ofSets] | |
| exact .inr hz | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] at hz ⊢ | |
| theorem equiv_of_bypass_right {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | |
| {d dl : ι → IGame.{u}} (hbb : ∀ i, {l | Set.range d ∪ r}ᴵ ≤ dl i) | |
| (hdl : ∀ i, dl i ∈ (d i).leftMoves) : | |
| {l | Set.range d ∪ r}ᴵ ≈ {l | (⋃ i, (dl i).rightMoves) ∪ r}ᴵ := by | |
| constructor | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] at hz ⊢ | |
| · intro z hz | |
| rw [rightMoves_ofSets] at hz | |
| obtain ⟨_, ⟨i, rfl⟩, hz⟩ | hz := hz | |
| · apply not_le_of_le_of_not_le (hbb i) | |
| exact lf_of_rightMove_le le_rfl hz | |
| · apply lf_of_rightMove_le le_rfl | |
| rw [rightMoves_ofSets] | |
| exact .inr hz | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] at hz ⊢ | |
| · intro z hz | |
| rw [rightMoves_ofSets] at hz | |
| obtain ⟨i, rfl⟩ | hz := hz | |
| · refine lf_of_le_leftMove ?_ (hdl i) | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| refine not_le_of_not_le_of_le ?_ (hbb i) | |
| apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] at hz ⊢ | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rw [rightMoves_ofSets] | |
| exact .inl (Set.mem_iUnion_of_mem i hz) | |
| · apply lf_of_rightMove_le le_rfl | |
| rw [rightMoves_ofSets] | |
| exact .inr hz | |
| theorem equiv_of_bypass_left {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | |
| {c cr : ι → IGame.{u}} (hbb : ∀ i, cr i ≤ {Set.range c ∪ l | r}ᴵ) | |
| (hcr : ∀ i, cr i ∈ (c i).rightMoves) : | |
| {Set.range c ∪ l | r}ᴵ ≈ {(⋃ i, (cr i).leftMoves) ∪ l | r}ᴵ := by | |
| constructor <;> dsimp <;> rw [le_iff_forall_lf] | |
| all_goals refine ⟨fun z hz ↦ ?_, fun z hz ↦ lf_rightMove hz⟩; rw [leftMoves_ofSets] at hz | |
| · obtain ⟨i, rfl⟩ | hz := hz | |
| · refine lf_of_rightMove_le ?_ (hcr i) | |
| rw [le_iff_forall_lf] | |
| refine ⟨fun z hz ↦ leftMove_lf ?_, fun z hz ↦ lf_rightMove_of_le (hbb i) hz⟩ | |
| rw [leftMoves_ofSets] | |
| exact .inl (Set.mem_iUnion_of_mem i hz) | |
| · apply leftMove_lf | |
| rw [leftMoves_ofSets] | |
| exact .inr hz | |
| · obtain ⟨-, ⟨i, rfl⟩, hz⟩ | hz := hz | |
| · exact not_le_of_not_le_of_le (leftMove_lf hz) (hbb i) | |
| · apply leftMove_lf | |
| rw [leftMoves_ofSets] | |
| exact .inr hz | |
| theorem equiv_of_bypass_right {ι : Type u} {l r : Set IGame.{u}} [Small.{u} l] [Small.{u} r] | |
| {d dl : ι → IGame.{u}} (hbb : ∀ i, {l | Set.range d ∪ r}ᴵ ≤ dl i) | |
| (hdl : ∀ i, dl i ∈ (d i).leftMoves) : | |
| {l | Set.range d ∪ r}ᴵ ≈ {l | (⋃ i, (dl i).rightMoves) ∪ r}ᴵ := by | |
| rw [← neg_equiv_neg_iff] | |
| simp_rw [neg_ofSets, Set.union_neg, Set.neg_range, Set.iUnion_neg, ← leftMoves_neg] | |
| apply equiv_of_bypass_left <;> intro i | |
| · rw [← IGame.neg_le_neg_iff] | |
| simpa [Set.neg_range] using hbb i | |
| · rw [rightMoves_neg, Set.mem_neg, neg_neg] | |
| exact hdl i |
tristan-f-r
reviewed
Jul 13, 2025
Comment on lines
112
to
162
| theorem equiv_of_gift_left {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | ||
| (hg : ∀ g ∈ gs, ¬{l | r}ᴵ ≤ g) : {l | r}ᴵ ≈ {gs ∪ l | r}ᴵ := by | ||
| constructor | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rw [leftMoves_ofSets] at hz ⊢ | ||
| exact .inr hz | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] at hz ⊢ | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| rw [leftMoves_ofSets] at hz | ||
| obtain hz | hz := hz | ||
| · exact hg z hz | ||
| · apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] at hz ⊢ | ||
|
|
||
| theorem equiv_of_gift_right {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | ||
| (hg : ∀ g ∈ gs, ¬g ≤ {l | r}ᴵ) : {l | r}ᴵ ≈ {l | gs ∪ r}ᴵ := by | ||
| constructor | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] at hz ⊢ | ||
| · intro z hz | ||
| rw [rightMoves_ofSets] at hz | ||
| obtain hz | hz := hz | ||
| · exact hg z hz | ||
| · apply lf_of_rightMove_le le_rfl | ||
| rwa [rightMoves_ofSets] | ||
| · dsimp | ||
| rw [le_iff_forall_lf] | ||
| constructor | ||
| · intro z hz | ||
| apply lf_of_le_leftMove le_rfl | ||
| rwa [leftMoves_ofSets] at hz ⊢ | ||
| · intro z hz | ||
| apply lf_of_rightMove_le le_rfl | ||
| rw [rightMoves_ofSets] at hz ⊢ | ||
| exact .inr hz |
Collaborator
There was a problem hiding this comment.
(The same golfing patterns above can be used here as well)
Suggested change
| theorem equiv_of_gift_left {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | |
| (hg : ∀ g ∈ gs, ¬{l | r}ᴵ ≤ g) : {l | r}ᴵ ≈ {gs ∪ l | r}ᴵ := by | |
| constructor | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rw [leftMoves_ofSets] at hz ⊢ | |
| exact .inr hz | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] at hz ⊢ | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| rw [leftMoves_ofSets] at hz | |
| obtain hz | hz := hz | |
| · exact hg z hz | |
| · apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] at hz ⊢ | |
| theorem equiv_of_gift_right {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | |
| (hg : ∀ g ∈ gs, ¬g ≤ {l | r}ᴵ) : {l | r}ᴵ ≈ {l | gs ∪ r}ᴵ := by | |
| constructor | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] at hz ⊢ | |
| · intro z hz | |
| rw [rightMoves_ofSets] at hz | |
| obtain hz | hz := hz | |
| · exact hg z hz | |
| · apply lf_of_rightMove_le le_rfl | |
| rwa [rightMoves_ofSets] | |
| · dsimp | |
| rw [le_iff_forall_lf] | |
| constructor | |
| · intro z hz | |
| apply lf_of_le_leftMove le_rfl | |
| rwa [leftMoves_ofSets] at hz ⊢ | |
| · intro z hz | |
| apply lf_of_rightMove_le le_rfl | |
| rw [rightMoves_ofSets] at hz ⊢ | |
| exact .inr hz | |
| theorem equiv_of_gift_left {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | |
| (hg : ∀ g ∈ gs, ¬{l | r}ᴵ ≤ g) : {l | r}ᴵ ≈ {gs ∪ l | r}ᴵ := by | |
| constructor | |
| all_goals dsimp; rw [le_iff_forall_lf]; constructor <;> intro z hz | |
| · apply leftMove_lf | |
| rw [leftMoves_ofSets] at hz ⊢ | |
| exact .inr hz | |
| · exact lf_rightMove hz | |
| · rw [leftMoves_ofSets] at hz | |
| obtain hz | hz := hz | |
| · exact hg z hz | |
| · apply leftMove_lf | |
| rwa [leftMoves_ofSets] | |
| · exact lf_rightMove hz | |
| theorem equiv_of_gift_right {gs l r : Set IGame.{u}} [Small.{u} gs] [Small.{u} l] [Small.{u} r] | |
| (hg : ∀ g ∈ gs, ¬g ≤ {l | r}ᴵ) : {l | r}ᴵ ≈ {l | gs ∪ r}ᴵ := by | |
| rw [← neg_equiv_neg_iff] | |
| simp_rw [neg_ofSets, Set.union_neg] | |
| apply equiv_of_gift_left | |
| intro g' hg' | |
| rw [← IGame.neg_le_neg_iff] | |
| simpa using hg (-g') hg' |
Owner
|
(I'd love to review this, can you please review the golfs first?) |
vihdzp
reviewed
Aug 22, 2025
vihdzp
reviewed
Dec 31, 2025
Owner
vihdzp
left a comment
vihdzp
left a comment
There was a problem hiding this comment.
This looks much better. Some small notes.
| import CombinatorialGames.Game.Order | ||
| import CombinatorialGames.Game.Ordinal | ||
| import CombinatorialGames.Game.Player | ||
| import CombinatorialGames.Game.Reductions |
Owner
There was a problem hiding this comment.
What do you think about putting this on the beginning of the Canonical file? That way we can use this in order to prove stuff about undominate/unreverse/canonical.
Contributor
Author
There was a problem hiding this comment.
I think we can add the import when the results are being used.
|
|
||
| namespace IGame | ||
| open Set | ||
|
|
Owner
There was a problem hiding this comment.
Suggested change
| variable {l r u v w : Set IGame.{u}} | |
| [Small.{u} l] [Small.{u} u] [Small.{u} r] [Small.{u} v] [Small.{u} w] | |
Contributor
Author
There was a problem hiding this comment.
It turns out some of those Small assumptions don't appear sometimes on the theorems
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
This reverts commit d7ea4ce.
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.