[Merged by Bors] - feat(set_theory/{pgame, surreal}): add `left_distrib_equiv` and `right_distrib_equiv` for pgames #7440

apurvnakade · 2021-05-02T14:56:23Z

and several other auxiliary lemmas.

Zulip thread

src/set_theory/surreal.lean

eric-wieser · 2021-05-06T16:59:43Z

src/set_theory/game.lean

-@[refl] theorem le_refl : ∀ x : game, x ≤ x :=
+theorem le_refl : ∀ x : game, x ≤ x :=
 by { rintro ⟨x⟩, apply pgame.le_refl }
-@[trans] theorem le_trans : ∀ x y z : game, x ≤ y → y ≤ z → x ≤ z :=
+theorem le_trans : ∀ x y z : game, x ≤ y → y ≤ z → x ≤ z :=


Does the linter reject these now?

The issue is not with the linter. There are type check errors in the calc mode proofs and refl proofs. Lean tries to use game.le_trans where it should be using pgame.le_trans.
Similarly, for refl.

There's an error here:

mathlib/src/set_theory/surreal.lean

Line 389 in 41674ba

calc w + y ≤ move_left x ix + y : add_le_add_right hix

and one here:

mathlib/src/set_theory/surreal.lean

Line 531 in 41674ba

le_refl := by { rintros ⟨_⟩, refl },

This worries me quite a bit - I don't see why lean at any point thinks these two are interchangeable

theorem game.le_trans (x y z : game) : x ≤ y → y ≤ z → x ≤ z theorem pgame.le_trans {x y z : pgame} : x ≤ y → y ≤ z → x ≤ z

Ah, here's the cause: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/norm_num.20can't.20solve.201.20.E2.89.A4.202/near/226015763

Thanks for finding this! This thread is unresolved though :(
Is there any workaround for this?

I wonder if there is some way to assign "priorities" to trans and refl...

Priorities wouldn't help, theproblem is that the refl tactic says "find me the refl lemma for has_le.le", not "find me the refl lemma for @has_le.le pgame".

Your choice to remove them was sensible here - but I'd recommend perhaps going further and either in this PR or a follow-up, removing all the refl and trans attributes about le and lt, and adding them back locally using local attribute [trans] pgame.le_trans etc (along with a link to that thread!).

I tried this, but it breaks all the calc proofs (and there are lots of them) in surreal.lean

Several calc proofs are about numeric so can't be moved to pgame.lean

src/set_theory/surreal.lean

semorrison · 2021-05-10T09:07:26Z

@apurvnakade, can you summarise the new results by providing a distrib surreal instance? I think it's good if we keep the instances in sync with the theorems.

semorrison · 2021-05-10T09:07:45Z

Either way, this is looking good to me and hopefully we can merge shortly.

apurvnakade · 2021-05-10T12:26:34Z

@apurvnakade, can you summarise the new results by providing a distrib surreal instance? I think it's good if we keep the instances in sync with the theorems.

There is still a missing numeric_mul lemma. I working on it's proof but the proof is turning out to be quite big.
My plan is to PR mul_assoc for pgames next so that we're done will all the theorems for pgames and then move on to numeric_mul.

apurvnakade · 2021-05-10T12:27:19Z

Right now, it is not possible to define mul for surreal numbers.

semorrison · 2021-05-11T06:13:31Z

bors merge

…t_distrib_equiv` for pgames (#7440) and several other auxiliary lemmas. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers)

bors · 2021-05-11T09:12:59Z

Pull request successfully merged into master.

Build succeeded:

apurvnakade added 10 commits May 1, 2021 00:17

Add equiv_of_mk_equiv.

f6c4bbf

Add local tactic.

18ec619

Add left_distrib and right_distrib.

2430404

Cleanup.

a61e204

Remove redundant lemma.

37f7e1b

Change equiv symbol.

bf02b99

Add pgame.le_refl.

6b6366b

Proof without set_theory.game

49aea38

Style cleanup.

c410edc

Minor edits.

34163c1

apurvnakade added the awaiting-review The author would like community review of the PR label May 2, 2021

Fix typo.

4166939

eric-wieser reviewed May 2, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 2, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

Style issues.

b6af842

semorrison reviewed May 5, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

semorrison reviewed May 5, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

semorrison reviewed May 5, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

semorrison reviewed May 5, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 5, 2021

apurvnakade added 2 commits May 4, 2021 23:21

Replace tactic + style fixes.

a3b7091

Remove add_{comm_}sub_relabelling lemmas.

e9db907

apurvnakade added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 5, 2021

apurvnakade added 5 commits May 5, 2021 00:46

Remove relabelling.sub_congr.

f3fb967

Golf.

a59e4de

Remove @[refl] and @[trans] tags.

138bcc3

Remove sub_congr.

bf9d541

Rewrite proofs using abel tactic.

0a6e44b

semorrison reviewed May 6, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

semorrison reviewed May 6, 2021

View reviewed changes

src/set_theory/surreal.lean Show resolved Hide resolved

semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 6, 2021

Add sub_congr and relabelling.sub_congr.

7e907dd

apurvnakade added awaiting-review The author would like community review of the PR WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR labels May 6, 2021

Add simp lemmas for quotient pgame.setoid.

95bcbdb

apurvnakade added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels May 6, 2021

apurvnakade added 2 commits May 6, 2021 11:57

Change def to abbreviation.

31e68ea

Remove whitespace.

57d868f

eric-wieser reviewed May 6, 2021

View reviewed changes

src/set_theory/surreal.lean Outdated Show resolved Hide resolved

Style fix.

41674ba

apurvnakade requested a review from eric-wieser May 8, 2021 13:06

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 11, 2021

bors bot changed the title ~~feat(set_theory/{pgame, surreal}): add left_distrib_equiv and right_distrib_equiv for pgames~~ [Merged by Bors] - feat(set_theory/{pgame, surreal}): add left_distrib_equiv and right_distrib_equiv for pgames May 11, 2021

bors bot closed this May 11, 2021

bors bot deleted the surreal_mul_distrib branch May 11, 2021 09:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add `left_distrib_equiv` and `right_distrib_equiv` for pgames #7440

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add `left_distrib_equiv` and `right_distrib_equiv` for pgames #7440

apurvnakade commented May 2, 2021

eric-wieser May 6, 2021

apurvnakade May 6, 2021 •

edited

apurvnakade May 6, 2021

eric-wieser May 10, 2021

eric-wieser May 10, 2021

apurvnakade May 10, 2021

apurvnakade May 10, 2021

eric-wieser May 10, 2021 •

edited

apurvnakade May 10, 2021

apurvnakade May 10, 2021

semorrison commented May 10, 2021

semorrison commented May 10, 2021

apurvnakade commented May 10, 2021

apurvnakade commented May 10, 2021

semorrison commented May 11, 2021

bors bot commented May 11, 2021

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add left_distrib_equiv and right_distrib_equiv for pgames #7440

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add left_distrib_equiv and right_distrib_equiv for pgames #7440

Conversation

apurvnakade commented May 2, 2021

Choose a reason for hiding this comment

apurvnakade May 6, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser May 10, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

semorrison commented May 10, 2021

semorrison commented May 10, 2021

apurvnakade commented May 10, 2021

apurvnakade commented May 10, 2021

semorrison commented May 11, 2021

bors bot commented May 11, 2021

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add `left_distrib_equiv` and `right_distrib_equiv` for pgames #7440

[Merged by Bors] - feat(set_theory/{pgame, surreal}): add `left_distrib_equiv` and `right_distrib_equiv` for pgames #7440

apurvnakade May 6, 2021 •

edited

eric-wieser May 10, 2021 •

edited