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] - chore: fix name *.Lf #7163

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: fix name *.Lf #7163

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 7 additions & 7 deletions Mathlib/SetTheory/Game/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,11 +98,11 @@ instance instPartialOrderGame : PartialOrder Game where
/-- The less or fuzzy relation on games.

If `0 ⧏ x` (less or fuzzy with), then Left can win `x` as the first player. -/
def Lf : Game → Game → Prop :=
Quotient.lift₂ PGame.Lf fun _ _ _ _ hx hy => propext (lf_congr hx hy)
#align game.lf SetTheory.Game.Lf
def LF : Game → Game → Prop :=
Quotient.lift₂ PGame.LF fun _ _ _ _ hx hy => propext (lf_congr hx hy)
#align game.lf SetTheory.Game.LF

local infixl:50 " ⧏ " => Lf
local infixl:50 " ⧏ " => LF

/-- On `Game`, simp-normal inequalities should use as few negations as possible. -/
@[simp]
Expand All @@ -118,8 +118,8 @@ theorem not_lf : ∀ {x y : Game}, ¬x ⧏ y ↔ y ≤ x := by
exact PGame.not_lf
#align game.not_lf SetTheory.Game.not_lf

-- porting note: had to replace ⧏ with Lf, otherwise cannot differentiate with the operator on PGame
instance : IsTrichotomous Game Lf :=
-- porting note: had to replace ⧏ with LF, otherwise cannot differentiate with the operator on PGame
instance : IsTrichotomous Game LF :=
⟨by
rintro ⟨x⟩ ⟨y⟩
change _ ∨ ⟦x⟧ = ⟦y⟧ ∨ _
Expand All @@ -136,7 +136,7 @@ theorem PGame.le_iff_game_le {x y : PGame} : x ≤ y ↔ (⟦x⟧ : Game) ≤
Iff.rfl
#align game.pgame.le_iff_game_le SetTheory.Game.PGame.le_iff_game_le

theorem PGame.lf_iff_game_lf {x y : PGame} : PGame.Lf x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
theorem PGame.lf_iff_game_lf {x y : PGame} : PGame.LF x y ↔ ⟦x⟧ ⧏ ⟦y⟧ :=
Iff.rfl
#align game.pgame.lf_iff_game_lf SetTheory.Game.PGame.lf_iff_game_lf

Expand Down
32 changes: 16 additions & 16 deletions Mathlib/SetTheory/Game/PGame.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -399,12 +399,12 @@ instance le : LE PGame :=
/-- The less or fuzzy relation on pre-games.

If `0 ⧏ x`, then Left can win `x` as the first player. -/
def Lf (x y : PGame) : Prop :=
def LF (x y : PGame) : Prop :=
¬y ≤ x
#align pgame.lf SetTheory.PGame.Lf
#align pgame.lf SetTheory.PGame.LF

@[inherit_doc]
scoped infixl:50 " ⧏ " => PGame.Lf
scoped infixl:50 " ⧏ " => PGame.LF

@[simp]
protected theorem not_le {x y : PGame} : ¬x ≤ y ↔ y ⧏ x :=
Expand All @@ -420,9 +420,9 @@ theorem _root_.LE.le.not_gf {x y : PGame} : x ≤ y → ¬y ⧏ x :=
not_lf.2
#align has_le.le.not_gf LE.le.not_gf

theorem Lf.not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x :=
theorem LF.not_ge {x y : PGame} : x ⧏ y → ¬y ≤ x :=
id
#align pgame.lf.not_ge SetTheory.PGame.Lf.not_ge
#align pgame.lf.not_ge SetTheory.PGame.LF.not_ge

/-- Definition of `x ≤ y` on pre-games, in terms of `⧏`.

Expand Down Expand Up @@ -454,7 +454,7 @@ The ordering here is chosen so that `or.inl` refer to moves by Left, and `or.inr
moves by Right. -/
theorem lf_iff_exists_le {x y : PGame} :
x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y := by
rw [Lf, le_iff_forall_lf, not_and_or]
rw [LF, le_iff_forall_lf, not_and_or]
simp
#align pgame.lf_iff_exists_le SetTheory.PGame.lf_iff_exists_le

Expand Down Expand Up @@ -581,8 +581,8 @@ instance : Trans (· ⧏ ·) (· ≤ ·) (· ⧏ ·) := ⟨lf_of_lf_of_le⟩
alias _root_.LE.le.trans_lf := lf_of_le_of_lf
#align has_le.le.trans_lf LE.le.trans_lf

alias Lf.trans_le := lf_of_lf_of_le
#align pgame.lf.trans_le SetTheory.PGame.Lf.trans_le
alias LF.trans_le := lf_of_lf_of_le
#align pgame.lf.trans_le SetTheory.PGame.LF.trans_le

@[trans]
theorem lf_of_lt_of_lf {x y z : PGame} (h₁ : x < y) (h₂ : y ⧏ z) : x ⧏ z :=
Expand All @@ -597,8 +597,8 @@ theorem lf_of_lf_of_lt {x y z : PGame} (h₁ : x ⧏ y) (h₂ : y < z) : x ⧏ z
alias _root_.LT.lt.trans_lf := lf_of_lt_of_lf
#align has_lt.lt.trans_lf LT.lt.trans_lf

alias Lf.trans_lt := lf_of_lf_of_lt
#align pgame.lf.trans_lt SetTheory.PGame.Lf.trans_lt
alias LF.trans_lt := lf_of_lf_of_lt
#align pgame.lf.trans_lt SetTheory.PGame.LF.trans_lt

theorem moveLeft_lf {x : PGame} : ∀ i, x.moveLeft i ⧏ x :=
le_rfl.moveLeft_lf
Expand Down Expand Up @@ -809,14 +809,14 @@ instance : Trans
((· ≤ ·) : PGame → PGame → Prop) where
trans := le_of_equiv_of_le

theorem Lf.not_equiv {x y : PGame} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
#align pgame.lf.not_equiv SetTheory.PGame.Lf.not_equiv
theorem LF.not_equiv {x y : PGame} (h : x ⧏ y) : ¬(x ≈ y) := fun h' => h.not_ge h'.2
#align pgame.lf.not_equiv SetTheory.PGame.LF.not_equiv

theorem Lf.not_equiv' {x y : PGame} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
#align pgame.lf.not_equiv' SetTheory.PGame.Lf.not_equiv'
theorem LF.not_equiv' {x y : PGame} (h : x ⧏ y) : ¬(y ≈ x) := fun h' => h.not_ge h'.1
#align pgame.lf.not_equiv' SetTheory.PGame.LF.not_equiv'

theorem Lf.not_gt {x y : PGame} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
#align pgame.lf.not_gt SetTheory.PGame.Lf.not_gt
theorem LF.not_gt {x y : PGame} (h : x ⧏ y) : ¬y < x := fun h' => h.not_ge h'.le
#align pgame.lf.not_gt SetTheory.PGame.LF.not_gt

theorem le_congr_imp {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) (h : x₁ ≤ y₁) : x₂ ≤ y₂ :=
hx.2.trans (h.trans hy.1)
Expand Down
18 changes: 9 additions & 9 deletions Mathlib/SetTheory/Game/Short.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,36 +274,36 @@ instance shortBit1 (x : PGame.{u}) [Short x] : Short (bit1 x) := by dsimp [bit1]
We build `Decidable (x ≤ y)` and `Decidable (x ⧏ y)` in a simultaneous induction.
Instances for the two projections separately are provided below.
-/
def leLfDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)
def leLFDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)
Copy link
Member

Choose a reason for hiding this comment

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

Not a big deal, but this name seems really quite weird. Do our naming conventions allow lelfDecidable? It might be worth asking on Zulip, but feel free to merge before getting an answer

bors d+

| mk xl xr xL xR, mk yl yr yL yR, shortx, shorty => by
constructor
· refine' @decidable_of_iff' _ _ mk_le_mk (id _)
apply @And.decidable _ _ ?_ ?_
· apply @Fintype.decidableForallFintype xl _ ?_ _
intro i
apply (leLfDecidable _ _).2
apply (leLFDecidable _ _).2
· apply @Fintype.decidableForallFintype yr _ ?_ _
intro i
apply (leLfDecidable _ _).2
apply (leLFDecidable _ _).2
· refine' @decidable_of_iff' _ _ mk_lf_mk (id _)
apply @Or.decidable _ _ ?_ ?_
· apply @Fintype.decidableExistsFintype yl _ ?_ _
intro i
apply (leLfDecidable _ _).1
apply (leLFDecidable _ _).1
· apply @Fintype.decidableExistsFintype xr _ ?_ _
intro i
apply (leLfDecidable _ _).1
apply (leLFDecidable _ _).1
-- Porting note: In Lean 3 `using_well_founded` didn't need this to be explicit.
termination_by leLfDecidable x y _ _ => Prod.mk x y
termination_by leLFDecidable x y _ _ => Prod.mk x y
-- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
#align pgame.le_lf_decidable SetTheory.PGame.leLfDecidable
#align pgame.le_lf_decidable SetTheory.PGame.leLFDecidable

instance leDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ≤ y) :=
(leLfDecidable x y).1
(leLFDecidable x y).1
#align pgame.le_decidable SetTheory.PGame.leDecidable

instance lfDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x ⧏ y) :=
(leLfDecidable x y).2
(leLFDecidable x y).2
#align pgame.lf_decidable SetTheory.PGame.lfDecidable

instance ltDecidable (x y : PGame.{u}) [Short x] [Short y] : Decidable (x < y) :=
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/SetTheory/Surreal/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -135,15 +135,15 @@ theorem le_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) :
not_lf.1 (lf_asymm ox oy h)
#align pgame.le_of_lf SetTheory.PGame.le_of_lf

alias Lf.le := le_of_lf
#align pgame.lf.le SetTheory.PGame.Lf.le
alias LF.le := le_of_lf
#align pgame.lf.le SetTheory.PGame.LF.le

theorem lt_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) : x < y :=
(lt_or_fuzzy_of_lf h).resolve_right (not_fuzzy_of_le (h.le ox oy))
#align pgame.lt_of_lf SetTheory.PGame.lt_of_lf

alias Lf.lt := lt_of_lf
#align pgame.lf.lt SetTheory.PGame.Lf.lt
alias LF.lt := lt_of_lf
#align pgame.lf.lt SetTheory.PGame.LF.lt

theorem lf_iff_lt {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y ↔ x < y :=
⟨fun h => h.lt ox oy, lf_of_lt⟩
Expand Down