Instance for `(quotient pgame.setoid)`

Stream: maths

[Apurva Nakade]

In set_theory/game.lean, game is defined as quotient pgame.setoid.
There is an instance add_comm_group game already defined there.

But the following throws an error:

instance : add_comm_group (quotient pgame.setoid) := by apply_instance

tactic.mk_instance failed to generate instance for
  add_comm_group (quotient pgame.setoid)`

I'm trying to define lemmas like

@[simp] lemma test (a b : pgame) : ⟦a + b⟧ = ⟦a⟧ + ⟦b⟧ := sorry

but I'm getting the same error - Lean is unable to find has_add instance for quotient pgame.setoid.

What's going on?

[Yakov Pechersky]

When you make the instance definition of instance add_comm_group game, that won't transfer over to quotient pgame.setoid because game is a different type. It is a type synonym. This allows us to place different instances on seemingly "same" types.

[Yakov Pechersky]

Like opposite orders -- check out docs#order_dual

[Yakov Pechersky]

You could transfer it over explicitly by instance : add_comm_group (quotient pgame.setoid) := game.add_comm_group

[Apurva Nakade]

I see, I thought the two were definitionally equal so the instances would automatically carry over. Thanks!

[Bhavik Mehta]

You can also use @[derive] to automatically transfer the instance, by putting @[derive add_comm_group] above the def of game

[Apurva Nakade]

@[derive] is throwing some weird errors. Should it be before somewhere else?

https://github.com/leanprover-community/mathlib/blob/9c86e38141b94bcd23665717f26c1da1622c59a7/src/set_theory/game.lean#L35

[Eric Wieser]

derive is a red herring here

[Eric Wieser]

Changing def game := quotient pgame.setoid to abbreviation game := quotient pgame.setoid would solve your problem, but might create new problems

[Eric Wieser]

You can only use derive for def foo := bar if bar already has the structure you want to derive

[Eric Wieser]

It doesn't work for structures that haven't been defined yet

[Apurva Nakade]

The first solution of explicitly defining the instance seems to be the best approach then.

[Eric Wieser]

abbreviation might be better if it doesn't break anything

[Eric Wieser]

Since then you don't need to do anything else

[Apurva Nakade]

Thanks! It worked, nothing broken so far.