Zulip Chat Archive

Stream: mathlib4

Topic: failed to synthesize Additive (Group G)


Winston Yin (尹維晨) (Jan 27 2023 at 03:34):

Why do I have to use French quotes to give Lean the instance of Additive (Group G), when Lean3 was able to synthesise it automatically?

import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Deprecated.Submonoid

variable {G : Type _} {H : Type _} {A : Type _} {a a₁ a₂ b c : G}
variable [Group G] [AddGroup A]

structure IsAddSubgroup (s : Set A) extends IsAddSubmonoid s : Prop where
  neg_mem {a} : a  s  -a  s

@[to_additive]
structure IsSubgroup (s : Set G) extends IsSubmonoid s : Prop where
  inv_mem {a} : a  s  a⁻¹  s

structure IsNormalAddSubgroup [AddGroup A] (s : Set A) extends IsAddSubgroup s : Prop where
  normal :  n  s,  g : A, g + n + -g  s

@[to_additive]
structure IsNormalSubgroup [Group G] (s : Set G) extends IsSubgroup s : Prop where
  normal :  n  s,  g : G, g * n * g⁻¹  s

theorem Additive.isAddSubgroup {s : Set G} (hs : IsSubgroup s) : @IsAddSubgroup (Additive G) _ s :=
  @IsAddSubgroup.mk (Additive G) _ _ (Additive.isAddSubmonoid hs.toIsSubmonoid) hs.inv_mem

theorem Additive.isNormalAddSubgroup [Group G] {s : Set G} (hs : IsNormalSubgroup s) :
    @IsNormalAddSubgroup (Additive G) _ s :=
  @IsNormalAddSubgroup.mk (Additive G) _ _ (Additive.isAddSubgroup hs.toIsSubgroup)
    (@IsNormalSubgroup.normal _ Group (Additive G)› _ hs)
    -- porting note: Lean needs help synthesising
    -- fails: (IsNormalSubgroup.normal hs)

Winston Yin (尹維晨) (Jan 27 2023 at 03:36):

There are a few such examples in deprecated.subgroup


Last updated: Dec 20 2023 at 11:08 UTC