## 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?

#### 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):

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):

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

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