Type classes

Stream: new members

[yuppie]

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]

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]

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]

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

[Johan Commelin]

That's why you get all the "field bla not provided" errors when you delete ..g

[yuppie]

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]

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

[Johan Commelin]

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]

Oh ok, thanks!

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Elvorfirilmathredia]

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]

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.