Zulip Chat Archive

Stream: new members

Topic: Type classes


view this post on Zulip 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!

view this post on Zulip 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 }

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Nov 27 2019 at 07:49):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 27 2019 at 08:24):

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

view this post on Zulip 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

view this post on Zulip yuppie (Nov 27 2019 at 08:27):

Oh ok, thanks!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 27 2019 at 08:50):

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

view this post on Zulip Patrick Massot (Nov 27 2019 at 08:51):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 27 2019 at 10:41):

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

view this post on Zulip 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"

view this post on Zulip 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 ...

view this post on Zulip 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