Zulip Chat Archive

Stream: maths

Topic: add_group to group


view this post on Zulip Kevin Buzzard (Jul 24 2020 at 19:01):

I'm really surprised this works. It came up when refactoring subgroups:

import tactic

example (A : Type) [add_group A] (x : A) (m n : ) :
gsmul (m+n) x = gsmul m x + gsmul n x := gpow_add x m n
/-
gpow_add : ∀ {G : Type} [_inst_1 : group G] (a : G) (m n : ℤ),
  a ^ (m + n) = a ^ m * a ^ n
-/

Lean has to infer G given x, and if it goes for G = A then it's not going to find the group instance because A is an add_group. But G=multiplicative A works. What makes Lean try that?

view this post on Zulip Jalex Stark (Jul 24 2020 at 19:10):

i'm not at my VSCode right now, but I think if there is an instance [add_group G] : group G := multiplicative G, then typeclass inference should just do it

view this post on Zulip Jalex Stark (Jul 24 2020 at 19:11):

(and of course for this to work we can only register multiplicative as an instance and not additive)

view this post on Zulip Yury G. Kudryashov (Jul 24 2020 at 19:54):

gsmul is defined as @gpow (multiplicative A) _ a n so Lean already has access to multiplicative A.


Last updated: May 14 2021 at 19:21 UTC