# Zulip Chat Archive

## Stream: new members

### Topic: Homework for "formalizing mathematics"

#### Laurent Bartholdi (Mar 16 2021 at 17:53):

Hi! I'm going through @Kevin Buzzard 's "formalizing mathematics" (wishing I were again an undergraduate), and stumbled already at week 1, part B. There's a lemma

`lemma union_subset_union (hWX : W ⊆ X) (hYZ : Y ⊆ Z) : W ∪ Y ⊆ X ∪ Z := ...`

which I could do, and the next exercise is `lemma union_subset_union_left (hXY : X ⊆ Y) : X ∪ Z ⊆ Y ∪ Z := ...`

. Now I would like to say it's a special case of union_subset_union; so the proof should be something like

```
begin
rw union_subset_union hXY (subset_refl Z)
end
```

Unfortunately none of the command I tried (rw, exact, apply, various combinations and variants) seem to work; and the homework solutions give a direct proof rather than apply the previous lemma. I thought that application of previous lemmas was done by rewriting, but obviously I'm missing something.

Meta-question: where do I find the answer to such questions without harassing everyone on Zulip? :)

#### Eric Wieser (Mar 16 2021 at 17:54):

`rw`

is for applying lemmas with an `=`

or an `iff`

in their statement. Yours is neither, but the goal state of the lemma you want to apply is exactly the same as the one you're aiming for; so you want the `apply`

tactic.

#### Eric Wieser (Mar 16 2021 at 17:55):

But since you've worked out the arguments already, you can use `exact`

instead

#### Laurent Bartholdi (Mar 16 2021 at 17:57):

@Eric Wieser wow, thanks for the quick reply! `exact`

is indeed something I tried; but `exact union_subset_union hXY (subset_refl Z)`

causes the error message `hXY has type X \subset Y : Prop but is expected to have type Type : Type1`

#### Thomas Browning (Mar 16 2021 at 18:04):

here's how I like to handle this sort of thing. Don't write the `exact`

right away. Start by writing `have key := union_subset_union,`

. Then you can see what `union_subset_union`

expects next. You can then add in the arguments one at a time. Once `key`

looks like your goal, you can switch to an exact statement.

#### Bryan Gin-ge Chen (Mar 16 2021 at 18:04):

(For ease of reference, I guess the worksheet in question is here: https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_1/Part_B_sets.lean )

#### Bryan Gin-ge Chen (Mar 16 2021 at 18:05):

Indeed, because there are round parentheses on line 5, `union_subset_union`

will require several additional arguments before `hXY`

. I think things should work if you insert a sufficient number of underscores before `hXY`

(the underscores tell Lean to try to infer the arguments automatically).

#### Adam Topaz (Mar 16 2021 at 18:16):

Here's a little animation of me going through this proof using `refine`

(similar to the suggestion of using `have`

that Thomas mentioned above)

out.gif

#### Laurent Bartholdi (Mar 16 2021 at 20:07):

Fantastic! For posterity, if one wants to stick with "exact", the answer is `exact union_subset_union Ω Y Z Z X hXY (subset_refl Ω Z),`

#### Bryan Gin-ge Chen (Mar 16 2021 at 20:14):

Usually a terminal `refine (something)`

can be replaced with `exact (something)`

, so I suspect `exact union_subset_union _ _ _ _ _ hXY (subset_refl _ _),`

works just as well.

#### Laurent Bartholdi (Mar 21 2021 at 10:38):

Okay, so I finished week 2 of the @Kevin Buzzard's course, which introduces groups and subgroups. I'm lost with syntax questions: for context Kevin defines

```
class group (G : Type) extends has_mul G, has_one G, has_inv G := /- group axioms -/
structure subgroup (G : Type) [group G] := (carrier : set G) /- and membership axioms/proofs for one mul, inv -/
```

I tried to add a few lemmas, but can't even get their statements right, and it seems that I'm confused between which things are sets, types, and properties. For example, how should one implement the follewing?

```
-- for every H : subgroup G, H.carrier is a group by itself
lemma subgroup_is_group (H : subgroup G) : group ↑H := sorry
```

I seemingly can construct some examples of subgroups, say the trivial subgroup and full group, but I don't see how they can be useful: I would have expected I could define a lemma `lemma trivial_is_subgroup {group G} : ({(1:G)} : subgroup G)`

, but the closest I can do is

```
-- for every group G, {1} is a subgroup
lemma trivial_subgroup : subgroup G := { carrier := {(1:G)}, one_mem' := sorry, mul_mem' := sorry, inv_mem' := sorry }
-- for every group G, G is a subgroup
lemma whole_group : subgroup G := { carrier := λ x, true, one_mem' := sorry, mul_mem' := sorry, inv_mem' := sorry }
```

so if at some moment in another proof I have a hypothesis `h : K = {1}`

, how will I conclude `⊢ K : subgroup G`

?

#### Sebastien Gouezel (Mar 21 2021 at 10:58):

You can never conclude `K : subgroup G`

from `h : K = {1}`

, because these objects don't have the same type: when you write `K = {1}`

, the type of `K`

is `set G`

, not `subgroup G`

. What you can hope to do is promote `K`

to a subgroup, i.e., claim that there is `K' : subgroup G`

such that the carrier of `K'`

is `K`

(which can be expressed with coercions as `(K' : set G) = K`

).

#### Kevin Buzzard (Mar 21 2021 at 11:00):

Your "lemma"s aren't lemmas because they're definitions. I agree that trying to work out the difference between types and terms and sets and etc is confusing, somehow the point of that class was just to show people what abstract mathematics looked like in lean.

#### Sebastien Gouezel (Mar 21 2021 at 11:00):

In practice, however, this is not how things are done: usually, it is much more efficient to work directly in `subgroup G`

(for which we have a lot of constructors, like: the kernel of a group morphism is by definition a subgroup of `G`

, not a subset of `G`

; the product of two subgroups is a subgroup of the product group, and so on).

#### Kevin Buzzard (Mar 21 2021 at 11:02):

Yes, the problem with using my home-made subgroup is that you then have to make all the machinery yourself. Of course this can be quite good fun :-) but one thing you've just realised you've needed is an extensionality lemma -- two subgroups are equal iff they have the same underlying subset.

#### Laurent Bartholdi (Mar 21 2021 at 11:31):

Great, I understand better why my attempts at the last two lemmas are useless. About the first: if I try

```
lemma subgroup_is_group (H : subgroup G) : group H := { mul_assoc := sorry, one_mul := sorry, mul_left_inv := sorry }
```

I'm told that lean

```
failed to synthesize type class instance for
G : Type,
_inst_1 : group G,
H : subgroup G
⊢ has_mul ↥H
```

but my understanding is that if I can get this to work and then `def commutative (group G) := ∀ x y, x*y = y*x`

then I should be able to prove `lemma sub_com (H : subgroup G) (C : commutative G) -> commutative (subgroup_is_group H)`

.

Can someone help me walk baby-steps along this? Thanks!

#### Scott Morrison (Mar 21 2021 at 11:37):

Given the last error message you got, I would go to the empty line above `lemma subgroup_is_group`

and start typing `instance (H : subgroup G) : has_mul H := ...`

#### Scott Morrison (Mar 21 2021 at 11:38):

because you need to tell Lean what multiplication you intend to use on `H`

.

#### Kevin Buzzard (Mar 21 2021 at 11:44):

I will write up a brief framework now which will show you how to do the things you want to do.

#### Kevin Buzzard (Mar 21 2021 at 12:08):

```
-- all within namespace `xena.subgroup`
-- treat a subgroup as a type in its own right
instance : has_coe_to_sort (subgroup G) := ⟨_, λ H, {g : G // g ∈ H}⟩
-- key things to know for the proofs below: a term of type `↥H` is a *pair*
-- consisting of a term `a : G` and a proof `ha : a ∈ H`.
-- If `x : ↥H` then you can do `cases x with a ha`
-- to get to the elements of the pair. If you don't want to take
-- `x` apart then `x.1` is the term of type `G` and `x.2` is the proof it's in `H`.
-- if you have `x y : ↥H` and want to reduce a proof of `x = y`
-- to a proof that the corresponding elements of `G` are equal
-- then you can do `cases x with a ha, cases y with b hb, ext, dsimp`
-- Also, because Lean has groups already, you will run into the
-- problem that `rw mul_assoc` will be ambiguous :-(
-- `rw xena.group.mul_assoc`. It is extremely difficult to fix
-- this without just using different names to the standard Lean
-- names, which is somehow not a good idea :-(
instance subgroup_is_group (H : subgroup G) : group ↥H :=
{ mul := λ a b, ⟨a.1 * b.1, H.mul_mem a.2 b.2⟩,
one := ⟨1, H.one_mem⟩,
inv := λ a, ⟨a.1⁻¹, H.inv_mem a.2⟩,
mul_assoc := begin
sorry
end,
one_mul := sorry,
mul_left_inv := sorry }
/-
To do this next one you need to know the basic API for sets. For
example
set.mem_singleton a : a ∈ {a}
set.mem_singleton_iff : a ∈ {b} ↔ a = b
You might want to just `open set` so that you don't have
to write "set." everywhere
-/
def bot : subgroup G := { carrier := {(1:G)},
one_mem' := begin
sorry
end,
mul_mem' := begin
sorry
end,
inv_mem' := sorry }
/-
To do this one, you need to know the basic API for `true`,
which is that you can prove it using the `trivial` tactic.
-/
def top : subgroup G :=
{ carrier := λ x, true,
one_mem' := begin
sorry
end,
mul_mem' := begin
sorry
end,
inv_mem' := sorry }
```

#### Kevin Buzzard (Mar 21 2021 at 12:14):

The weird type-theoretic thing which is new here is that the way to make `G`

into a group in Lean is `(G : Type) [h : group G]`

. We don't normally name `h`

because a system called the type class inference system looks after `h`

for us. `h`

is all the data associated with the group structure on `G`

, i.e. the multiplication, the proof that it is associative etc. Here `G`

is a type and `h`

is a term. The Lean model for $a\in G$ is `a : G`

-- the terms of the type `G`

.

Subgroups however are not like this. If `H : subgroup G`

then `H`

is a *term* not a type, so `h : H`

does not even make sense. the first thing we need to do is to tell Lean how to make terms of type `subgroup G`

into types in their own right -- this is the "coercion to Sort" (Sort means "Type or Prop", the two universes in my course). Once we have this, one has to learn to control the fact that terms of type `↥H`

(the "coerced H") are *pairs* consisting of an element of $G$ and a proof that it's in the subgroup $H$.

I did this stuff in week 2 because I thought it would be good to get onto something which was "recognisably mathematics" very early on, however I realised when I did it that there was very limited scope for further exploration because I had not talked about several other things. I'm currently reworking all the material and one thing I discovered during the course was that I really wished I had done stuff with sets a lot earlier, so next year when I teach this I will probably do a bunch of set stuff before I start on groups.

Let me know if you have any more questions Laurent!

#### Sebastien Gouezel (Mar 21 2021 at 12:51):

Also, let me point out that there is some flexibility in the design space. Instead of defining a type `subgroup G`

, we could work with subsets of `G`

and use a predicate `is_subgroup K`

(where `K : set G`

and `is_subgroup K`

asserts that the subset `K`

contains `1`

and is stable under multiplication and inversion). The first approach, in which `K : subgroup G`

is more than a subset, is called the *bundled* approach, while the second one, in which ones uses subsets and asserts something on them, is called the unbundled approach. In mathlib, we started with the unbundled approach (which corresponds more closely to what you were trying to do, Laurent), but after a lot of experimentations and refactors we came to the conclusion that the bundled approach is more efficient, so that's the way things are now set up.

#### Laurent Bartholdi (Mar 21 2021 at 17:52):

@Kevin Buzzard thanks, that helps a lot -- though I can't try your code directly: ```
instance : has_coe_to_sort (subgroup G) := ⟨_, λ H, {g : G // g ∈ H}⟩
instance subgroup_is_group (H : subgroup G) : group ↑H := {...}
```

produces at the "`↑H`

"

```
failed to synthesize type class instance for
G : Type,
_inst_1 : group G,
H : subgroup G
⊢ has_lift_t (subgroup G) Type
```

I feared it was an interference of the previous `instance : has_coe (subgroup G) (set G) := ⟨λ H, H.carrier⟩`

but commenting that line out doesn't help. Trying random variations of `instance : has_lift_t (subgroup G) := sorry`

(I feel like a monkey at a typewriter) doesn't work either.

Do I understand correctly that the original coercion, in your work2 file, forced a subgroup into a subset (in which \in tests membership), while the new one forces a subgroup into a group (in which : tests membership)? Then I guess both are incompatible. I also guess that it's a good idea to define as many "coercions" as possible, in that lean/mathlib will silently apply them in many useful cases.

#### Eric Wieser (Mar 21 2021 at 17:54):

I think you have the wrong up arrow!

#### Eric Wieser (Mar 21 2021 at 17:54):

You want `\u-|`

not `\u`

#### Eric Wieser (Mar 21 2021 at 17:59):

You want `\u-|`

not `\u`

#### Eric Wieser (Mar 21 2021 at 18:00):

You want `\u-|`

not `\u`

#### Kevin Buzzard (Mar 21 2021 at 18:17):

Yes, there are unfortunately three kinds of coercions (things that mathematicians would just regard as invisible) -- you can coerce a term to another term (e.g. `H : subgroup G`

into `H : set G`

), a term into a type (e.g. `H : subgroup G`

into `\u-| H : Type`

) or a term into a function (e.g. we use this for group homomorphisms -- there is a type `monoid_hom G H`

and if `f : monoid_hom G H`

then `\u= f : G -> H`

).

#### Laurent Bartholdi (Mar 21 2021 at 21:05):

I feel I'm making good progress... I could finish all of Kevin's goals. Here's now what I tried -- and got stuck at:

```
class is_commutative K [group K] : Prop := (comm : ∀ (x:K) (y:K), x*y = y*x)
lemma is_commutative_def (K : Type) [group K] : is_commutative K ↔ ∀ (x:K) (y:K), x*y = y*x := ⟨λ K, K.comm, λ K, ⟨K⟩⟩
lemma sub_of_com (h0 : is_commutative G) (H : subgroup G) : is_commutative ↥H := begin
rw is_commutative_def,
rw is_commutative_def at h0,
intros x y,
ext, dsimp,
exact h0
end
```

There is an error at the `dsimp`

which cannot progress (while it went fine in the `subgroup_is_group`

example). Comments and advice on the style are most welcome (in particular, does one really have to define a class and a lemma?)

#### Scott Morrison (Mar 21 2021 at 21:33):

#mwe?

#### Scott Morrison (Mar 21 2021 at 21:35):

This presumably isn't matching your definitions, but this works:

```
import group_theory.subgroup
class is_commutative' K [group K] : Prop := (comm : ∀ (x:K) (y:K), x*y = y*x)
lemma is_commutative_def (K : Type) [group K] : is_commutative' K ↔ ∀ (x:K) (y:K), x*y = y*x :=
⟨λ K, K.comm, λ K, ⟨K⟩⟩
variables (G : Type) [group G]
lemma sub_of_com (h0 : is_commutative' G) (H : subgroup G) : is_commutative' ↥H := begin
rw is_commutative_def,
rw is_commutative_def at h0,
intros x y,
ext, dsimp,
exact h0 _ _,
end
```

#### Kevin Buzzard (Mar 21 2021 at 22:20):

`dsimp`

is failing because it can't simplify what it sees, namely `↑(x * y) = ↑(y * x)`

. This doesn't mean it can't be simplified, it just means that not enough things have been tagged with `simp`

and proved with `refl`

. Here's a proof:

```
lemma sub_of_com (h0 : is_commutative G) (H : subgroup G) : is_commutative ↥H := begin
rw is_commutative_def,
rw is_commutative_def at h0,
intros x y,
ext,
change x.1 * y.1 = y.1 * x.1,
exact h0 x.1 y.1
end
```

The `change`

tactic will replace any goal by a definitionally equal goal. Note however that the `exact`

tactic works up to definitional equality, so you can just delete the `change`

line and the proof still compiles.

#### Kevin Buzzard (Mar 21 2021 at 22:28):

As for style, this is tricky. You could make an `is_commutative`

class on top of `group`

, or you could just make a new class `comm_group`

extending `group`

. But you're being inconsistent with your lemma -- if `is_commutative`

is to be a class then you should write `[is_commutative G]`

instead of `(h0 : is_commutative G)`

and now it's a pain to access `h0`

. The way one would usually do this is something like this:

```
class is_commutative K [group K] : Prop := (comm : ∀ (x:K) (y:K), x*y = y*x)
lemma is_commutative_def (K : Type) [group K] [h : is_commutative K] :
∀ (x:K) (y:K), x*y = y*x := h.comm
lemma sub_of_com [is_commutative G] (H : subgroup G) : is_commutative ↥H := begin
constructor,
have h0 := is_commutative_def G,
intros x y,
ext,
apply h0,
end
```

Let me stress that even for a professional mathematician, writing definitions in Lean is hard. In my course I supplied every definition and just let the students fill in the theorems. Writing definitions means you have to deal with the idea of implementation issues -- e.g. there are 11 definitions of a discrete valuation ring on Wikipedia, but Lean only wants one, so there is a decision to be made here. Other issues such as structure or class, type or term etc etc just make matters worse. There are plenty of things I still don't understand here myself, for example I know that in mathlib they don't do commutativity the way you're suggesting -- they make an entirely new class `comm_group`

extending `group`

-- but I would not be able to tell you why.

#### Yakov Pechersky (Mar 21 2021 at 22:38):

In addition, there are various relations like `commute x y`

that can state that some specific elements commute for some op, even if in general they do not. So stating that elements in a normal subgroup commute might use that `commute`

.

#### Yakov Pechersky (Mar 21 2021 at 22:38):

#### Mario Carneiro (Mar 21 2021 at 23:32):

you should write [is_commutative G] instead of (h0 : is_commutative G) and now it's a pain to access h0.

One would normally write `is_commutative.comm`

to access h0 (not `h0.comm`

)

Last updated: Dec 20 2023 at 11:08 UTC