## Stream: new members

### Topic: Structure extends

#### Martin Dvořák (Aug 05 2021 at 08:51):

In the exercises from "Lean for the Curious Mathematician" (2020), there is this example of extending a structure.

structure Group :=
(G : Type*)
(op : G → G → G)
(infix * := op) -- temporary notation * for op, just inside this structure declaration
(op_assoc' : ∀ (x y z : G), (x * y) * z = x * (y * z))
(id : G)
(notation 1 := id) -- temporary notation 1 for id, just inside this structure declaration
(id_op' : ∀ (x : G), 1 * x = x)
(inv : G → G)
(postfix ⁻¹ := inv) -- temporary notation ⁻¹ for inv, just inside this structure declaration
(op_left_inv' : ∀ (x : G), x⁻¹ * x = 1)

structure CommGroup extends Group :=
(infix * := op)
(op_comm : ∀ (x y : G), x * y = y * x)

def rat_Group : Group :=
{ G := ℚ,
op := (+), -- you can put parentheses around an infix operation to talk about the operation itself.
id := 0,
inv := λ x, -x,

def rat_CommGroup : CommGroup :=
{ G := ℚ, op_comm := add_comm, ..rat_Group }


Why do we have to explicitly state G := ℚ on the last line but not the other fields? What is the general rule?

Is it because CommGroup contains a field op_comm which refers to G explicitly? Do these have to be always restated before instantiating the new fields and before calling ..superstructure in the definition?

#### Ruben Van de Velde (Aug 05 2021 at 08:57):

The problem seems to be that add_comm is itself a theorem about all add_comm_semigroups G, so Lean can't figure out what to fill in forG. It seems to be fine with a hint:

def rat_CommGroup : CommGroup :=
{ op_comm := @add_comm ℚ _, ..rat_Group }


or:

lemma add_comm' (a b : ℚ) : a + b = b + a := add_comm _ _

def rat_CommGroup : CommGroup :=
{ op_comm := add_comm', ..rat_Group }


Last updated: Dec 20 2023 at 11:08 UTC