confusion between equivalence and instance setoid

Stream: new members

[Gabin Kolly]

I'm currently trying to port SetTheory/Game/Basic.lean to learn, and the theorem

theorem PGame.equiv_iff_game_eq {x y : PGame} : (x ≈ y) ↔ ⟦x⟧ = ⟦y⟧ :=
  (@Quotient.eq' _ _ x y).symm

is not accepted because there are two possible interpretations for ≈. However, these two interpretations are the same: they are the function defined in PGame.lean, and the corresponding instance HasEquiv, deduced from the instance Setoid (defined in Basic.Lean), which is defined using the same equivalence. What should I do in this situation? More generally, how can we determine locally the meaning of notations?

[Kyle Miller]

These seems to be a design error in the original file.

I would suggest removing ≈ notation from PGame.lean (so remove the scoped infixl:0 " ≈ " => PGame.Equiv) and then move the setoid instance from Game.lean to PGame.lean

You should be able to write something like

instance instSetoid : Setoid PGame :=
⟨PGame.equiv, refl, symm, trans⟩

right after the IsEquiv instance that's immediately after the scoped infixl

[Gabin Kolly]

Thank you! Is there a way to keep the doc for ≈? Now there is no more explanation of the definition when hovering over the symbol.

[Kyle Miller]

I don't think so, at least for now (it'd be neat if you could get type-specific documentation for generic notation)

[Kyle Miller]

You should write a porting note that you deleted the scoped notation due to notation overloading, and you can add to the note that this causes the PGame.equiv docstring to not show up on hover

[Gabin Kolly]

Other question about notation: Lean4 gets confused sometimes with the notation [[...]] for elements in the quotient, and is not sure of which quotient I'm talking about. Is there a way to indicate locally which quotient it should consider?
For the moment I fix this by expliciting which type it is, for example

theorem PGame.le_iff_game_le {x y : PGame} : x ≤ y ↔ (⟦x⟧ : Game) ≤ ⟦y⟧ :=
  Iff.rfl

But having to add this for each theorem is a bit cumbersome.

[Kyle Miller]

It looks like the definition of quotient notation changed in Lean 4 and there's no porting note, so I'm not sure why

[Kyle Miller]

It used to take the setoid as an instance argument, but now it takes it as an explicit argument solved by unification

[Kyle Miller]

That explains why you need to give the expected type

[Gabin Kolly]

I used

notation:max "⟦" arg "⟧" => Quot.mk PGame.setoid arg

And it seems to work fine

Edit: no it does not work in fact.

[Kyle Miller]

We probably should fix this. I've left a comment at the PR that introduced the change; https://github.com/leanprover-community/mathlib4/pull/559/files#r1204394250

[Anne Baanen]

I can't recall making an explicit definition to use mk over mk' for the notation, but there were quite a few issues with inferring the instance for mk' that there weren't for mk. So let's see if that situation improved.

[Kyle Miller]

There also seems to be a general design principle that it's better to make your own quotient constructor than use Quotient.mk directly. Maybe we should have Game.mk : PGame -> Game that's defined to be Quotient.mk'?

[Kyle Miller]

The issue is that Game isn't syntactically the same as Quotient _ PGame, so the square bracket notation doesn't give you a Game per se

[Kyle Miller]

x ≤ y ↔ Game.mk x ≤ Game.mk y isn't so bad

[Kyle Miller]

@Anne Baanen It might also be fine leaving a porting note, because it might be better this way rather than relying on global setoid instances

[Kyle Miller]

In fact, I think this means I can remove the really bad one that Sym2 uses finally

[Anne Baanen]

That's a good point, that Setoid should often not have global instances. I'll leave a porting note that explains the difference and says that we have not yet decided whether to use an instance parameter or not.

[Anne Baanen]

!4#4306