# Zulip Chat Archive

## Stream: new members

### Topic: Type classes

#### yuppie (Nov 23 2019 at 21:23):

Hey everybody,

I am trying to prove a basic algebra homework. If every element of a group (actually not necessarily finite, but let's forget about that) has order 2 the group is commutative. Here is my code snippet:

import algebra.group.basic import group_theory.order_of_element variable α : Type variables [group α] [decidable_eq α] [fintype α] lemma T : (∀ x : α, x*x = 1) → ∀ x y : α, x*y=y*x := begin intros h a b, have k := h a, have l := h (a*b), have m := h b, have o := mul_left_inj a, cases o with p q, apply p, cases (mul_right_inj b) with p q, apply p, rw mul_assoc, rw mul_assoc, rw m, rw mul_one, rw k, rw mul_assoc, rw mul_assoc, rw ←mul_assoc, rw l, end theorem U : (∀ x : α, order_of x = 2) → comm_group α := begin intro, have mul_comm : comm_group α := sorry, exact mul_comm end

The lemma T type checks (ok it might not be pretty but it works). But I wanted to rewrite it in a way that looks more "native" (how you would find it on a exercise sheet). And I tried theorem U but somehow I don't really get the type class comm_group (or type classes in general). How do you repair this?

Thanks for your help!

#### Alex J. Best (Nov 23 2019 at 22:27):

Here is what I would do, I shortened `T`

a bit by using a new lemma fixed the statement of `U`

and try to explain typeclasses a little, hope it helps!

variable {α : Type} variables [group α] [decidable_eq α] [fintype α] -- this is a useful lemma, it is used 3 times even in the on paper proof lemma W {x : α} (h : x^2 = 1) : x = x⁻¹ := begin have := congr_arg ((*) (x⁻¹)) h, -- multiply by x⁻¹ rwa [pow_two, inv_mul_cancel_left, mul_one] at this, end lemma T (h : ∀ x : α, x^2 = 1) (x y : α) : x * y = y * x := begin have : ∀ x : α, x = x⁻¹ := λ x, W (h x), -- our lemma applies here call it `this` -- instead of using this we can just write W (h (blah)) explicitly everywhere if we want have l := this (x * y), rwa [mul_inv_rev, ← this x, ← this y] at l, -- (a*b)⁻¹ = b⁻¹ *a⁻¹ and our lemma twice end -- the original formulation order_of x = 2 is bad, the order of 1 is always 1 -- so no such groups existed! instead we want the order to be divide 2 lemma Q (h : ∀ x : α, order_of x ∣ 2) : ∀ x : α, x^2 = 1 := λ x, begin cases (h x), rw [h_1, pow_mul, pow_order_of_eq_one, one_pow], -- use whatever divisibility we have end -- to add a typeclass for α we define an instance of it -- in fact to give a comm_group we have to give the group structure -- and the statement that multiplication commutes, so we assume a given group structure -- [group α] like normal, but we name it g [g : group α], so we can refer to it -- this is the last line ..g it says "use the group structure coming from g" -- so we just have to prove commutativity by combining our lemmas instance order_two_comm_group [g : group α] (h : ∀ x : α, order_of x ∣ 2) : comm_group α := { mul_comm := T (Q h), ..g }

#### yuppie (Nov 27 2019 at 07:47):

Hey, thanks for the answer!

It works like a charm but I cannot find any documentation about this `..g`

syntax. Is it syntactic sugar for something else and has an alternative name? Moreover when I delete the last line

..g

I get the following error message:

/home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'mul' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'mul_assoc' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'one' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'one_mul' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'mul_one' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'inv' was not provided /home/double-curly.lean:36:0: error: invalid structure value { ... }, field 'mul_left_inv' was not provided /home/double-curly.lean:37:14: error: type mismatch at field 'mul_comm' T (Q h) has type ∀ (x y : α), x * y = y * x but is expected to have type ∀ (a b : α), a * b = b * a

The last two expressions - don't they have the same type?

#### Johan Commelin (Nov 27 2019 at 07:48):

About `..g`

: It roughly means "for fields that I didn't bother to tell you, just copy them from `g`

"

#### Johan Commelin (Nov 27 2019 at 07:49):

That's why you get all the "field `bla`

not provided" errors when you delete `..g`

#### yuppie (Nov 27 2019 at 08:23):

I thought that it roughly means that. But do you know where this is explained in more detail? What about the error message complaining about the different naming of variables? Why does that pop up?

#### Johan Commelin (Nov 27 2019 at 08:24):

No, I've never read the documentation... so I can't help you there.

#### Johan Commelin (Nov 27 2019 at 08:24):

The different variable names shouldn't matter. It's likely something else that's wrong under the hood. I agree that the second error is confusing and unhelpful

#### yuppie (Nov 27 2019 at 08:27):

Oh ok, thanks!

#### Patrick Massot (Nov 27 2019 at 08:50):

Where did you look for documentation? It's explained in the chapter of TPIL about structure: https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#objects

#### Patrick Massot (Nov 27 2019 at 08:50):

The confusing error message is probably because you have two multiplications on the same type.

#### Patrick Massot (Nov 27 2019 at 08:51):

But it's hard to tell without code we could test.

#### Mario Carneiro (Nov 27 2019 at 10:41):

What the error isn't telling you is that the `*`

in the first case has a type class instance that is constructed from the missing fields, but since you didn't provide the fields it put `sorry`

in for the type class, while it is expecting a structure literal (which is what shows up in the "official" type for `mul_comm`

)

#### Mario Carneiro (Nov 27 2019 at 10:41):

Basically it is error compounding - the first few errors cause more errors down the line

#### Kevin Buzzard (Nov 27 2019 at 11:14):

In short, "field mul not provided" also means "don't take anything I say about multiplication seriously after this point"

#### Elvorfirilmathredia (Nov 27 2019 at 19:09):

variable {α : Type} variables [group α] [decidable_eq α] [fintype α] -- this is a useful lemma, it is used 3 times even in the on paper proof lemma W {x : α} (h : x^2 = 1) : x = x⁻¹ := begin have := congr_arg ((*) (x⁻¹)) h, -- multiply by x⁻¹ rwa [pow_two, inv_mul_cancel_left, mul_one] at this, end

I'm still getting used to Lean so this is probably a stupid question, but why can I not write `have := congr_arg (group.mul (x⁻¹)) h`

?

Hm, `has_mul.mul`

works ...

#### Kevin Buzzard (Nov 27 2019 at 19:13):

import data.fintype variable {α : Type} variables [group α] [decidable_eq α] [fintype α] -- this is a useful lemma, it is used 3 times even in the on paper proof lemma W {x : α} (h : x^2 = 1) : x = x⁻¹ := begin have := congr_arg (group.mul (x⁻¹)) h, change x⁻¹ * (x ^ 2) = x⁻¹ * 1 at this, rwa [pow_two, inv_mul_cancel_left, mul_one] at this, end

[sorry if someone else posted, I'm on the underground with sporadic reception]. `rw`

works with syntactic equality not definitional equality.

Last updated: May 18 2021 at 17:44 UTC