Homework for "formalizing mathematics"

Stream: new members

[Laurent Bartholdi]

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]

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]

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

[Laurent Bartholdi]

@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]

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]

(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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

-- 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]

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]

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]

@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]

I think you have the wrong up arrow!

[Eric Wieser]

You want \u-| not \u

[Eric Wieser]

You want \u-| not \u

[Eric Wieser]

You want \u-| not \u

[Kevin Buzzard]

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]

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]

#mwe?

[Scott Morrison]

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]

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]

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]

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]

docs#commute

[Mario Carneiro]

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)