Zulip Chat Archive

Stream: maths

Topic: Instance for `(quotient pgame.setoid)`


view this post on Zulip Apurva Nakade (May 06 2021 at 14:59):

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?

view this post on Zulip Yakov Pechersky (May 06 2021 at 15:01):

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.

view this post on Zulip Yakov Pechersky (May 06 2021 at 15:01):

Like opposite orders -- check out docs#order_dual

view this post on Zulip Yakov Pechersky (May 06 2021 at 15:02):

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

view this post on Zulip Apurva Nakade (May 06 2021 at 15:09):

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

view this post on Zulip Bhavik Mehta (May 06 2021 at 15:15):

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

view this post on Zulip Apurva Nakade (May 06 2021 at 15:30):

@[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

view this post on Zulip Eric Wieser (May 06 2021 at 15:36):

derive is a red herring here

view this post on Zulip Eric Wieser (May 06 2021 at 15:37):

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

view this post on Zulip Eric Wieser (May 06 2021 at 15:38):

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

view this post on Zulip Eric Wieser (May 06 2021 at 15:38):

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

view this post on Zulip Apurva Nakade (May 06 2021 at 15:42):

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

view this post on Zulip Eric Wieser (May 06 2021 at 15:54):

abbreviation might be better if it doesn't break anything

view this post on Zulip Eric Wieser (May 06 2021 at 15:54):

Since then you don't need to do anything else

view this post on Zulip Apurva Nakade (May 06 2021 at 15:57):

Thanks! It worked, nothing broken so far.


Last updated: Jun 17 2021 at 17:28 UTC